The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the FP division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 1234 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 1037 | 506948.197 | 506921.04 | 1037 | 20 | 1017 | 197 | 137 | 48 | |
| 2018-CVC4n | 0 | 880 | 722150.807 | 722220.702 | 880 | 10 | 870 | 354 | 260 | 4 | |
| CVC4 | 0 | 865 | 643828.961 | 643879.555 | 865 | 10 | 855 | 369 | 254 | 9 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 179 | 4129.212 | 2878.785 | 179 | 0 | 179 | 1055 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 1037 | 506987.757 | 506914.63 | 1037 | 20 | 1017 | 197 | 137 | 48 | |
| 2018-CVC4n | 0 | 880 | 722233.327 | 722210.342 | 880 | 10 | 870 | 354 | 260 | 4 | |
| CVC4 | 0 | 865 | 643910.121 | 643867.345 | 865 | 10 | 855 | 369 | 254 | 9 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 179 | 4129.212 | 2878.785 | 179 | 0 | 179 | 1055 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 20 | 1516.418 | 1516.735 | 20 | 20 | 0 | 1214 | 137 | 48 |
| 2018-CVC4n | 0 | 10 | 24020.056 | 24020.054 | 10 | 10 | 0 | 1224 | 260 | 4 |
| CVC4 | 0 | 10 | 24022.688 | 24022.688 | 10 | 10 | 0 | 1224 | 254 | 9 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 66.95 | 47.676 | 0 | 0 | 0 | 1234 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 1017 | 176651.752 | 176577.957 | 1017 | 0 | 1017 | 217 | 137 | 48 |
| 2018-CVC4n | 0 | 870 | 357413.271 | 357390.287 | 870 | 0 | 870 | 364 | 260 | 4 |
| CVC4 | 0 | 855 | 279087.432 | 279044.657 | 855 | 0 | 855 | 379 | 254 | 9 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 179 | 3589.085 | 2501.181 | 179 | 0 | 179 | 1055 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 870 | 10130.353 | 10084.222 | 870 | 17 | 853 | 364 | 305 | 48 | |
| 2018-CVC4n | 0 | 794 | 12016.346 | 11987.323 | 794 | 10 | 784 | 440 | 436 | 4 | |
| CVC4 | 0 | 786 | 9666.161 | 9665.26 | 786 | 10 | 776 | 448 | 333 | 9 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 179 | 4129.212 | 2878.785 | 179 | 0 | 179 | 1055 | 0 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.