Difference between revisions of "SMT 1.4 Performance Results"
From Event-B
Jump to navigationJump to searchimported>Nicolas (Created page with "In SMT plug-in 1.4.0, the following bundled provers have been upgraded: * veriT (v2016) * CVC4 (v1.4) * Z3 (v4.5) This has led to globally improve the rate of automatically d...") |
imported>Nicolas (add images) |
||
| Line 3: | Line 3: | ||
* CVC4 (v1.4) | * CVC4 (v1.4) | ||
* Z3 (v4.5) | * Z3 (v4.5) | ||
| + | Note: CVC3 is still bundled but remains in the same version (v2.4.1) as in SMT 1.3. | ||
This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually. | This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually. | ||
| − | |||
| − | [[File: | + | The following picture shows the discharged POs for each project of the performance benchmark: |
| + | |||
| + | [[File:SMT_1.4_Perf_Discharged_POs.png]] | ||
This next image focuses on the remaining POs: | This next image focuses on the remaining POs: | ||
| − | [[File: | + | [[File:SMT_1.4_Perf_Remaining_POs.png]] |
[[Category:Plugin]] | [[Category:Plugin]] | ||
[[Category:User documentation]] | [[Category:User documentation]] | ||
Revision as of 09:48, 7 September 2017
In SMT plug-in 1.4.0, the following bundled provers have been upgraded:
- veriT (v2016)
- CVC4 (v1.4)
- Z3 (v4.5)
Note: CVC3 is still bundled but remains in the same version (v2.4.1) as in SMT 1.3.
This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually.
The following picture shows the discharged POs for each project of the performance benchmark:
This next image focuses on the remaining POs:
