The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_AUFBV division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 41 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices 2.6.2 | Yices 2.6.2 | Yices 2.6.2 | Yices 2.6.2 | Yices 2.6.2 |
| 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 | 38 | 7610.364 | 7611.728 | 38 | 7 | 31 | 3 | 3 | 0 | |
| Z3n | 0 | 38 | 9823.537 | 9820.223 | 38 | 6 | 32 | 3 | 3 | 0 | |
| Boolector | 0 | 32 | 16.484 | 16.493 | 32 | 6 | 26 | 9 | 0 | 0 | |
| Poolector | 0 | 32 | 46.707 | 18.085 | 32 | 6 | 26 | 9 | 0 | 0 | |
| 2018-CVC4n | 0 | 32 | 22957.184 | 23088.189 | 32 | 6 | 26 | 9 | 9 | 0 | |
| CVC4 | 0 | 32 | 23514.085 | 23657.38 | 32 | 6 | 26 | 9 | 9 | 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 | 38 | 7611.514 | 7611.568 | 38 | 7 | 31 | 3 | 3 | 0 | |
| Z3n | 0 | 38 | 9824.307 | 9820.123 | 38 | 6 | 32 | 3 | 3 | 0 | |
| Boolector | 0 | 32 | 16.484 | 16.493 | 32 | 6 | 26 | 9 | 0 | 0 | |
| Poolector | 0 | 32 | 46.707 | 18.085 | 32 | 6 | 26 | 9 | 0 | 0 | |
| 2018-CVC4n | 0 | 32 | 23079.294 | 23087.759 | 32 | 6 | 26 | 9 | 9 | 0 | |
| CVC4 | 0 | 32 | 23647.855 | 23656.93 | 32 | 6 | 26 | 9 | 9 | 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 | 7 | 235.901 | 235.935 | 7 | 7 | 0 | 34 | 3 | 0 |
| Boolector | 0 | 6 | 0.154 | 0.159 | 6 | 6 | 0 | 35 | 0 | 0 |
| Poolector | 0 | 6 | 1.231 | 1.235 | 6 | 6 | 0 | 35 | 0 | 0 |
| Z3n | 0 | 6 | 2400.441 | 2400.441 | 6 | 6 | 0 | 35 | 3 | 0 |
| 2018-CVC4n | 0 | 6 | 2400.568 | 2400.566 | 6 | 6 | 0 | 35 | 9 | 0 |
| CVC4 | 0 | 6 | 2400.585 | 2400.583 | 6 | 6 | 0 | 35 | 9 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 32 | 7423.866 | 7419.682 | 32 | 0 | 32 | 9 | 3 | 0 |
| Yices 2.6.2 | 0 | 31 | 7375.613 | 7375.633 | 31 | 0 | 31 | 10 | 3 | 0 |
| Boolector | 0 | 26 | 16.33 | 16.334 | 26 | 0 | 26 | 15 | 0 | 0 |
| Poolector | 0 | 26 | 45.476 | 16.85 | 26 | 0 | 26 | 15 | 0 | 0 |
| 2018-CVC4n | 0 | 26 | 20678.725 | 20687.192 | 26 | 0 | 26 | 15 | 9 | 0 |
| CVC4 | 0 | 26 | 21247.27 | 21256.347 | 26 | 0 | 26 | 15 | 9 | 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 | 35 | 167.933 | 167.94 | 35 | 6 | 29 | 6 | 6 | 0 | |
| Boolector | 0 | 32 | 16.484 | 16.493 | 32 | 6 | 26 | 9 | 0 | 0 | |
| Poolector | 0 | 32 | 46.707 | 18.085 | 32 | 6 | 26 | 9 | 0 | 0 | |
| CVC4 | 0 | 31 | 257.645 | 257.64 | 31 | 6 | 25 | 10 | 10 | 0 | |
| 2018-CVC4n | 0 | 31 | 257.694 | 257.689 | 31 | 6 | 25 | 10 | 10 | 0 | |
| Z3n | 0 | 31 | 264.868 | 260.109 | 31 | 6 | 25 | 10 | 10 | 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.