The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDT division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 1223 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | Alt-Ergo |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 420 | 1014599.95 | 1026503.857 | 420 | 101 | 319 | 803 | 803 | 0 | |
| 2019-CVC4n | 0 | 400 | 1052619.543 | 1075890.886 | 400 | 83 | 317 | 823 | 823 | 0 | |
| Vampire | 0 | 289 | 1145764.967 | 1127406.298 | 289 | 0 | 289 | 934 | 934 | 0 | |
| Alt-Ergo | 0 | 286 | 1059548.866 | 1051576.119 | 286 | 0 | 286 | 937 | 856 | 18 | |
| UltimateEliminator+MathSAT | 0 | 0 | 3996.763 | 2815.692 | 0 | 0 | 0 | 1223 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 420 | 1024172.89 | 1026466.907 | 420 | 101 | 319 | 803 | 803 | 0 | |
| 2019-CVC4n | 0 | 400 | 1074414.77 | 1075841.186 | 400 | 83 | 317 | 823 | 823 | 0 | |
| Vampire | 0 | 327 | 1226988.307 | 1113189.021 | 327 | 14 | 313 | 896 | 896 | 0 | |
| Alt-Ergo | 0 | 296 | 1114919.496 | 1045077.232 | 296 | 0 | 296 | 927 | 846 | 18 | |
| UltimateEliminator+MathSAT | 0 | 0 | 3996.763 | 2815.692 | 0 | 0 | 0 | 1223 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 101 | 46891.639 | 49061.871 | 101 | 101 | 0 | 1122 | 803 | 0 |
| 2019-CVC4n | 0 | 83 | 92433.841 | 93578.963 | 83 | 83 | 0 | 1140 | 823 | 0 |
| Vampire | 0 | 14 | 159981.61 | 120977.842 | 14 | 14 | 0 | 1209 | 896 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 337.099 | 250.028 | 0 | 0 | 0 | 1223 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 79377.302 | 79262.682 | 0 | 0 | 0 | 1223 | 846 | 18 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 319 | 62881.252 | 63005.036 | 319 | 0 | 319 | 904 | 803 | 0 |
| 2019-CVC4n | 0 | 317 | 67580.929 | 67862.223 | 317 | 0 | 317 | 906 | 823 | 0 |
| Vampire | 0 | 313 | 145406.587 | 77820.149 | 313 | 0 | 313 | 910 | 896 | 0 |
| Alt-Ergo | 0 | 296 | 105411.867 | 79571.622 | 296 | 0 | 296 | 927 | 846 | 18 |
| UltimateEliminator+MathSAT | 0 | 0 | 1165.814 | 811.635 | 0 | 0 | 0 | 1223 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Alt-Ergo | 0 | 265 | 22771.587 | 21884.671 | 265 | 0 | 265 | 958 | 879 | 18 | |
| 2019-CVC4n | 0 | 258 | 23376.306 | 23375.239 | 258 | 5 | 253 | 965 | 965 | 0 | |
| CVC4 | 0 | 255 | 23468.693 | 23468.759 | 255 | 5 | 250 | 968 | 968 | 0 | |
| Vampire | 0 | 235 | 27037.1 | 24578.254 | 235 | 0 | 235 | 988 | 988 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 4017.481 | 2811.951 | 0 | 0 | 0 | 1223 | 1 | 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.