The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ABV division in the Challenge Track (non-incremental).
Page generated on 2019-07-23 17:57:29 +0000
Benchmarks: 7 Time Limit: 43200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Boolector | Boolector | Boolector | — | Poolector |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Boolector | 0 | 7 | 258.318 | 258.33 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Poolector | 0 | 7 | 970.72 | 270.965 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 | 0 | 7 | 4255.126 | 4255.697 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Z3n | 0 | 5 | 151567.622 | 151576.42 | 5 | 5 | 0 | 2 | 2 | 0 | |
| 2018-Boolectorn | 0 | 1 | 106.1 | 107.157 | 1 | 1 | 0 | 6 | 0 | 0 | |
| CVC4 | 0 | 0 | 302255.1 | 302400.2 | 0 | 0 | 0 | 7 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Boolector | 0 | 7 | 258.318 | 258.33 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Poolector | 0 | 7 | 970.72 | 270.965 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Yices 2.6.2 | 0 | 7 | 4255.126 | 4255.697 | 7 | 7 | 0 | 0 | 0 | 0 | |
| Z3n | 0 | 5 | 151572.322 | 151576.22 | 5 | 5 | 0 | 2 | 2 | 0 | |
| 2018-Boolectorn | 0 | 1 | 106.1 | 107.157 | 1 | 1 | 0 | 6 | 0 | 0 | |
| CVC4 | 0 | 0 | 302306.4 | 302400.0 | 0 | 0 | 0 | 7 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Boolector | 0 | 7 | 258.318 | 258.33 | 7 | 7 | 0 | 0 | 0 | 0 |
| Poolector | 0 | 7 | 970.72 | 270.965 | 7 | 7 | 0 | 0 | 0 | 0 |
| Yices 2.6.2 | 0 | 7 | 4255.126 | 4255.697 | 7 | 7 | 0 | 0 | 0 | 0 |
| Z3n | 0 | 5 | 151572.322 | 151576.22 | 5 | 5 | 0 | 2 | 2 | 0 |
| 2018-Boolectorn | 0 | 1 | 106.1 | 107.157 | 1 | 1 | 0 | 6 | 0 | 0 |
| CVC4 | 0 | 0 | 302306.4 | 302400.0 | 0 | 0 | 0 | 7 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Boolectorn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Boolector | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| CVC4 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 7 | 0 |
| Poolector | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Yices 2.6.2 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 0 | 0 |
| Z3n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 7 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Poolector | 0 | 4 | 313.123 | 144.972 | 4 | 4 | 0 | 3 | 3 | 0 | |
| Boolector | 0 | 3 | 143.778 | 143.781 | 3 | 3 | 0 | 4 | 4 | 0 | |
| 2018-Boolectorn | 0 | 0 | 37.269 | 38.322 | 0 | 0 | 0 | 7 | 1 | 0 | |
| CVC4 | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 0 | |
| Yices 2.6.2 | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 0 | |
| Z3n | 0 | 0 | 168.0 | 168.0 | 0 | 0 | 0 | 7 | 7 | 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.