The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LIRA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +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 | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7 | 232.486 | 117.555 | 7 | 1 | 6 | 0 | 0 | 0 |
| z3-4.8.17n | 0 | 6 | 1276.672 | 1276.838 | 6 | 1 | 5 | 1 | 1 | 0 |
| Yices2 | 0 | 6 | 1476.732 | 1476.83 | 6 | 1 | 5 | 1 | 1 | 0 |
| cvc5 | 0 | 6 | 2173.608 | 2174.162 | 6 | 1 | 5 | 1 | 1 | 0 |
| veriT | 0 | 5 | 2404.693 | 2405.132 | 5 | 1 | 4 | 2 | 2 | 0 |
| MathSATn | 0 | 5 | 2407.982 | 2408.343 | 5 | 1 | 4 | 2 | 2 | 0 |
| smtinterpol | 0 | 4 | 3930.84 | 3769.155 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7 | 232.486 | 117.555 | 7 | 1 | 6 | 0 | 0 | 0 |
| z3-4.8.17n | 0 | 6 | 1276.732 | 1276.728 | 6 | 1 | 5 | 1 | 1 | 0 |
| Yices2 | 0 | 6 | 1476.792 | 1476.81 | 6 | 1 | 5 | 1 | 1 | 0 |
| cvc5 | 0 | 6 | 2174.018 | 2174.142 | 6 | 1 | 5 | 1 | 1 | 0 |
| veriT | 0 | 5 | 2405.053 | 2405.052 | 5 | 1 | 4 | 2 | 2 | 0 |
| MathSATn | 0 | 5 | 2408.212 | 2408.213 | 5 | 1 | 4 | 2 | 2 | 0 |
| smtinterpol | 0 | 4 | 3930.84 | 3769.155 | 4 | 1 | 3 | 3 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 1 | 0.076 | 0.076 | 1 | 1 | 0 | 0 | 6 | 1 | 0 |
| MathSATn | 0 | 1 | 0.191 | 0.191 | 1 | 1 | 0 | 0 | 6 | 2 | 0 |
| z3-4.8.17n | 0 | 1 | 0.292 | 0.291 | 1 | 1 | 0 | 0 | 6 | 1 | 0 |
| 2019-Par4n | 0 | 1 | 0.006 | 0.298 | 1 | 1 | 0 | 0 | 6 | 0 | 0 |
| veriT | 0 | 1 | 2.442 | 2.443 | 1 | 1 | 0 | 0 | 6 | 2 | 0 |
| cvc5 | 0 | 1 | 4.228 | 4.229 | 1 | 1 | 0 | 0 | 6 | 1 | 0 |
| smtinterpol | 0 | 1 | 18.404 | 6.234 | 1 | 1 | 0 | 0 | 6 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 6 | 232.48 | 117.257 | 6 | 0 | 6 | 0 | 1 | 0 | 0 |
| z3-4.8.17n | 0 | 5 | 1276.439 | 1276.438 | 5 | 0 | 5 | 1 | 1 | 1 | 0 |
| Yices2 | 0 | 5 | 1476.716 | 1476.734 | 5 | 0 | 5 | 1 | 1 | 1 | 0 |
| cvc5 | 0 | 5 | 2169.79 | 2169.913 | 5 | 0 | 5 | 1 | 1 | 1 | 0 |
| veriT | 0 | 4 | 2402.61 | 2402.61 | 4 | 0 | 4 | 2 | 1 | 2 | 0 |
| MathSATn | 0 | 4 | 2408.021 | 2408.022 | 4 | 0 | 4 | 2 | 1 | 2 | 0 |
| smtinterpol | 0 | 3 | 3912.436 | 3762.921 | 3 | 0 | 3 | 3 | 1 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 5 | 48.422 | 48.424 | 5 | 1 | 4 | 2 | 2 | 0 |
| z3-4.8.17n | 0 | 5 | 50.442 | 50.434 | 5 | 1 | 4 | 2 | 2 | 0 |
| 2019-Par4n | 0 | 5 | 50.746 | 50.54 | 5 | 1 | 4 | 2 | 2 | 0 |
| veriT | 0 | 5 | 53.053 | 53.052 | 5 | 1 | 4 | 2 | 2 | 0 |
| MathSATn | 0 | 5 | 56.212 | 56.213 | 5 | 1 | 4 | 2 | 2 | 0 |
| cvc5 | 0 | 5 | 65.709 | 65.71 | 5 | 1 | 4 | 2 | 2 | 0 |
| smtinterpol | 0 | 3 | 130.973 | 108.888 | 3 | 1 | 2 | 4 | 4 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.