The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LIRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 7 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7 | 222.249 | 111.967 | 7 | 1 | 6 | 0 | 0 | 0 | |
| z3n | 0 | 6 | 1338.104 | 1338.137 | 6 | 1 | 5 | 1 | 1 | 0 | |
| Yices2 | 0 | 6 | 1341.479 | 1341.605 | 6 | 1 | 5 | 1 | 1 | 0 | |
| Yices2-fixedn | 0 | 6 | 1342.579 | 1342.697 | 6 | 1 | 5 | 1 | 1 | 0 | |
| MathSAT5n | 0 | 5 | 2405.291 | 2405.771 | 5 | 1 | 4 | 2 | 2 | 0 | |
| CVC4 | 0 | 5 | 2405.58 | 2406.499 | 5 | 1 | 4 | 2 | 2 | 0 | |
| SMTInterpol-fixedn | 0 | 4 | 3734.913 | 3689.836 | 4 | 1 | 3 | 3 | 3 | 0 | |
| SMTInterpol | 0 | 4 | 3735.389 | 3688.632 | 4 | 1 | 3 | 3 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7 | 222.249 | 111.967 | 7 | 1 | 6 | 0 | 0 | 0 | |
| z3n | 0 | 6 | 1338.104 | 1338.137 | 6 | 1 | 5 | 1 | 1 | 0 | |
| Yices2 | 0 | 6 | 1341.539 | 1341.575 | 6 | 1 | 5 | 1 | 1 | 0 | |
| Yices2-fixedn | 0 | 6 | 1342.669 | 1342.677 | 6 | 1 | 5 | 1 | 1 | 0 | |
| MathSAT5n | 0 | 5 | 2405.701 | 2405.701 | 5 | 1 | 4 | 2 | 2 | 0 | |
| CVC4 | 0 | 5 | 2406.45 | 2406.449 | 5 | 1 | 4 | 2 | 2 | 0 | |
| SMTInterpol | 0 | 4 | 3735.389 | 3688.632 | 4 | 1 | 3 | 3 | 3 | 0 | |
| SMTInterpol-fixedn | 0 | 4 | 3734.913 | 3689.836 | 4 | 1 | 3 | 3 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 1 | 0.07 | 0.07 | 1 | 1 | 0 | 6 | 1 | 0 |
| Yices2-fixedn | 0 | 1 | 0.071 | 0.071 | 1 | 1 | 0 | 6 | 1 | 0 |
| MathSAT5n | 0 | 1 | 0.289 | 0.289 | 1 | 1 | 0 | 6 | 2 | 0 |
| z3n | 0 | 1 | 0.312 | 0.312 | 1 | 1 | 0 | 6 | 1 | 0 |
| 2019-Par4n | 0 | 1 | 0.006 | 0.334 | 1 | 1 | 0 | 6 | 0 | 0 |
| CVC4 | 0 | 1 | 1.138 | 1.137 | 1 | 1 | 0 | 6 | 2 | 0 |
| SMTInterpol-fixedn | 0 | 1 | 46.762 | 28.627 | 1 | 1 | 0 | 6 | 3 | 0 |
| SMTInterpol | 0 | 1 | 50.935 | 29.17 | 1 | 1 | 0 | 6 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 6 | 222.243 | 111.633 | 6 | 0 | 6 | 1 | 0 | 0 |
| z3n | 0 | 5 | 1337.792 | 1337.824 | 5 | 0 | 5 | 2 | 1 | 0 |
| Yices2 | 0 | 5 | 1341.469 | 1341.505 | 5 | 0 | 5 | 2 | 1 | 0 |
| Yices2-fixedn | 0 | 5 | 1342.598 | 1342.605 | 5 | 0 | 5 | 2 | 1 | 0 |
| CVC4 | 0 | 4 | 2405.312 | 2405.312 | 4 | 0 | 4 | 3 | 2 | 0 |
| MathSAT5n | 0 | 4 | 2405.412 | 2405.412 | 4 | 0 | 4 | 3 | 2 | 0 |
| SMTInterpol | 0 | 3 | 3684.454 | 3659.463 | 3 | 0 | 3 | 4 | 3 | 0 |
| SMTInterpol-fixedn | 0 | 3 | 3688.151 | 3661.209 | 3 | 0 | 3 | 4 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2-fixedn | 0 | 5 | 48.358 | 48.361 | 5 | 1 | 4 | 2 | 2 | 0 | |
| Yices2 | 0 | 5 | 48.358 | 48.361 | 5 | 1 | 4 | 2 | 2 | 0 | |
| z3n | 0 | 5 | 50.931 | 50.932 | 5 | 1 | 4 | 2 | 2 | 0 | |
| 2019-Par4n | 0 | 5 | 52.689 | 51.076 | 5 | 1 | 4 | 2 | 2 | 0 | |
| MathSAT5n | 0 | 5 | 53.701 | 53.701 | 5 | 1 | 4 | 2 | 2 | 0 | |
| CVC4 | 0 | 5 | 54.45 | 54.449 | 5 | 1 | 4 | 2 | 2 | 0 | |
| SMTInterpol | 0 | 2 | 125.591 | 122.057 | 2 | 0 | 2 | 5 | 5 | 0 | |
| SMTInterpol-fixedn | 0 | 2 | 125.739 | 122.069 | 2 | 0 | 2 | 5 | 5 | 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.