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 2019-07-23 17:56:09 +0000
Benchmarks: 7 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Yices 2.6.2 | Par4 | Yices 2.6.2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 7 | 226.017 | 113.799 | 7 | 1 | 6 | 0 | 0 | 0 | |
| 2018-Z3n | 0 | 6 | 2463.29 | 2463.589 | 6 | 1 | 5 | 1 | 1 | 0 | |
| Yices 2.6.2 | 0 | 6 | 2504.257 | 2504.683 | 6 | 1 | 5 | 1 | 1 | 0 | |
| Z3n | 0 | 6 | 2638.019 | 2638.353 | 6 | 1 | 5 | 1 | 1 | 0 | |
| CVC4 | 0 | 6 | 3474.956 | 3476.105 | 6 | 1 | 5 | 1 | 1 | 0 | |
| SMTInterpol | 0 | 4 | 7275.17 | 7238.009 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 7 | 226.017 | 113.799 | 7 | 1 | 6 | 0 | 0 | 0 | |
| 2018-Z3n | 0 | 6 | 2463.49 | 2463.499 | 6 | 1 | 5 | 1 | 1 | 0 | |
| Yices 2.6.2 | 0 | 6 | 2504.637 | 2504.653 | 6 | 1 | 5 | 1 | 1 | 0 | |
| Z3n | 0 | 6 | 2638.229 | 2638.273 | 6 | 1 | 5 | 1 | 1 | 0 | |
| CVC4 | 0 | 6 | 3475.656 | 3476.085 | 6 | 1 | 5 | 1 | 1 | 0 | |
| SMTInterpol | 0 | 4 | 7275.17 | 7238.009 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 1 | 0.087 | 0.087 | 1 | 1 | 0 | 6 | 1 | 0 |
| 2018-Z3n | 0 | 1 | 0.326 | 0.327 | 1 | 1 | 0 | 6 | 1 | 0 |
| Par4 | 0 | 1 | 0.006 | 0.33 | 1 | 1 | 0 | 6 | 0 | 0 |
| Z3n | 0 | 1 | 0.409 | 0.409 | 1 | 1 | 0 | 6 | 1 | 0 |
| CVC4 | 0 | 1 | 0.958 | 0.958 | 1 | 1 | 0 | 6 | 1 | 0 |
| SMTInterpol | 0 | 1 | 19.932 | 7.038 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 6 | 226.012 | 113.469 | 6 | 0 | 6 | 1 | 0 | 0 |
| 2018-Z3n | 0 | 5 | 2463.163 | 2463.172 | 5 | 0 | 5 | 2 | 1 | 0 |
| Yices 2.6.2 | 0 | 5 | 2504.551 | 2504.567 | 5 | 0 | 5 | 2 | 1 | 0 |
| Z3n | 0 | 5 | 2637.82 | 2637.864 | 5 | 0 | 5 | 2 | 1 | 0 |
| CVC4 | 0 | 5 | 3474.697 | 3475.127 | 5 | 0 | 5 | 2 | 1 | 0 |
| SMTInterpol | 0 | 3 | 7255.238 | 7230.971 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 5 | 48.481 | 48.481 | 5 | 1 | 4 | 2 | 2 | 0 | |
| 2018-Z3n | 0 | 5 | 50.751 | 50.751 | 5 | 1 | 4 | 2 | 2 | 0 | |
| Par4 | 0 | 5 | 52.247 | 50.799 | 5 | 1 | 4 | 2 | 2 | 0 | |
| Z3n | 0 | 5 | 52.624 | 52.624 | 5 | 1 | 4 | 2 | 2 | 0 | |
| CVC4 | 0 | 5 | 55.456 | 55.455 | 5 | 1 | 4 | 2 | 2 | 0 | |
| SMTInterpol | 0 | 3 | 122.93 | 105.5 | 3 | 1 | 2 | 4 | 4 | 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.