The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the ALIA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 19 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| SMTInterpol | SMTInterpol | SMTInterpol | Alt-Ergo | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 19 | 1.165 | 1.166 | 19 | 1 | 18 | 0 | 0 | 0 | |
| Z3n | 0 | 19 | 1.244 | 1.244 | 19 | 1 | 18 | 0 | 0 | 0 | |
| SMTInterpol | 0 | 19 | 1092.681 | 978.138 | 19 | 1 | 18 | 0 | 0 | 0 | |
| CVC4 | 0 | 18 | 4.744 | 4.735 | 18 | 0 | 18 | 1 | 0 | 0 | |
| Alt-Ergo | 0 | 18 | 2409.881 | 2404.416 | 18 | 0 | 18 | 1 | 1 | 0 | |
| Vampire | 0 | 13 | 18018.486 | 15312.524 | 13 | 0 | 13 | 6 | 6 | 0 | |
| veriT | 0 | 4 | 35996.46 | 36000.729 | 4 | 0 | 4 | 15 | 15 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 28908.211 | 28859.186 | 0 | 0 | 0 | 19 | 12 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 28946.248 | 28876.786 | 0 | 0 | 0 | 19 | 12 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 28949.546 | 28877.51 | 0 | 0 | 0 | 19 | 12 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 19 | 1.165 | 1.166 | 19 | 1 | 18 | 0 | 0 | 0 | |
| Z3n | 0 | 19 | 1.244 | 1.244 | 19 | 1 | 18 | 0 | 0 | 0 | |
| SMTInterpol | 0 | 19 | 1092.681 | 978.138 | 19 | 1 | 18 | 0 | 0 | 0 | |
| CVC4 | 0 | 18 | 4.744 | 4.735 | 18 | 0 | 18 | 1 | 0 | 0 | |
| Alt-Ergo | 0 | 18 | 2409.881 | 2404.416 | 18 | 0 | 18 | 1 | 1 | 0 | |
| Vampire | 0 | 15 | 28678.916 | 14507.914 | 15 | 0 | 15 | 4 | 4 | 0 | |
| veriT | 0 | 4 | 36000.07 | 36000.069 | 4 | 0 | 4 | 15 | 15 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 44351.318 | 27591.446 | 0 | 0 | 0 | 19 | 9 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 45313.206 | 27841.39 | 0 | 0 | 0 | 19 | 9 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 39040.021 | 27967.956 | 0 | 0 | 0 | 19 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 1 | 0.055 | 0.055 | 1 | 1 | 0 | 18 | 0 | 0 |
| Z3n | 0 | 1 | 0.056 | 0.056 | 1 | 1 | 0 | 18 | 0 | 0 |
| SMTInterpol | 0 | 1 | 1.383 | 0.59 | 1 | 1 | 0 | 18 | 0 | 0 |
| CVC4 | 0 | 0 | 0.279 | 0.277 | 0 | 0 | 0 | 19 | 0 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 3.344 | 2.269 | 0 | 0 | 0 | 19 | 10 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 3.295 | 2.359 | 0 | 0 | 0 | 19 | 9 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 3.39 | 2.363 | 0 | 0 | 0 | 19 | 9 | 0 |
| Alt-Ergo | 0 | 0 | 2400.0 | 2400.0 | 0 | 0 | 0 | 19 | 1 | 0 |
| Vampire | 0 | 0 | 2400.0 | 2400.0 | 0 | 0 | 0 | 19 | 4 | 0 |
| veriT | 0 | 0 | 2400.0 | 2400.0 | 0 | 0 | 0 | 19 | 15 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 18 | 1.11 | 1.111 | 18 | 0 | 18 | 1 | 0 | 0 |
| Z3n | 0 | 18 | 1.187 | 1.188 | 18 | 0 | 18 | 1 | 0 | 0 |
| Alt-Ergo | 0 | 18 | 9.881 | 4.416 | 18 | 0 | 18 | 1 | 1 | 0 |
| CVC4 | 0 | 18 | 4.465 | 4.458 | 18 | 0 | 18 | 1 | 0 | 0 |
| SMTInterpol | 0 | 18 | 1091.298 | 977.547 | 18 | 0 | 18 | 1 | 0 | 0 |
| Vampire | 0 | 15 | 26278.916 | 12107.914 | 15 | 0 | 15 | 4 | 4 | 0 |
| veriT | 0 | 4 | 33600.07 | 33600.069 | 4 | 0 | 4 | 15 | 15 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 44348.023 | 27589.087 | 0 | 0 | 0 | 19 | 9 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 45309.816 | 27839.027 | 0 | 0 | 0 | 19 | 9 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 39036.677 | 27965.687 | 0 | 0 | 0 | 19 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 19 | 1.165 | 1.166 | 19 | 1 | 18 | 0 | 0 | 0 | |
| Z3n | 0 | 19 | 1.244 | 1.244 | 19 | 1 | 18 | 0 | 0 | 0 | |
| CVC4 | 0 | 18 | 4.744 | 4.735 | 18 | 0 | 18 | 1 | 0 | 0 | |
| Alt-Ergo | 0 | 18 | 33.881 | 28.416 | 18 | 0 | 18 | 1 | 1 | 0 | |
| SMTInterpol | 0 | 14 | 230.497 | 176.726 | 14 | 1 | 13 | 5 | 5 | 0 | |
| Vampire | 0 | 5 | 364.996 | 343.786 | 5 | 0 | 5 | 14 | 14 | 0 | |
| veriT | 0 | 4 | 360.07 | 360.069 | 4 | 0 | 4 | 15 | 15 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 344.452 | 332.342 | 0 | 0 | 0 | 19 | 13 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 343.827 | 333.439 | 0 | 0 | 0 | 19 | 13 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 344.049 | 333.44 | 0 | 0 | 0 | 19 | 13 | 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.