The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFBV division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 223 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 | 220 | 19120.64 | 19122.442 | 220 | 133 | 87 | 3 | 3 | 0 | |
| Boolector | 0 | 217 | 25475.296 | 25477.144 | 217 | 133 | 84 | 6 | 6 | 0 | |
| 2018-Boolectorn | 0 | 213 | 2039.953 | 2040.274 | 213 | 132 | 81 | 10 | 0 | 0 | |
| CVC4 | 0 | 213 | 30579.127 | 30519.568 | 213 | 132 | 81 | 10 | 10 | 0 | |
| Poolector | 0 | 211 | 43664.445 | 32580.204 | 211 | 133 | 78 | 12 | 12 | 0 | |
| Z3n | 0 | 198 | 66301.091 | 66305.626 | 198 | 132 | 66 | 25 | 25 | 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 | 220 | 19121.27 | 19122.372 | 220 | 133 | 87 | 3 | 3 | 0 | |
| Poolector | 0 | 218 | 59220.165 | 23944.483 | 218 | 133 | 85 | 5 | 5 | 0 | |
| Boolector | 0 | 217 | 25475.496 | 25476.974 | 217 | 133 | 84 | 6 | 6 | 0 | |
| 2018-Boolectorn | 0 | 213 | 2039.953 | 2040.274 | 213 | 132 | 81 | 10 | 0 | 0 | |
| CVC4 | 0 | 213 | 30582.327 | 30519.228 | 213 | 132 | 81 | 10 | 10 | 0 | |
| Z3n | 0 | 198 | 66305.021 | 66304.916 | 198 | 132 | 66 | 25 | 25 | 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 | 133 | 143.623 | 143.632 | 133 | 133 | 0 | 90 | 3 | 0 |
| Poolector | 0 | 133 | 2252.227 | 589.354 | 133 | 133 | 0 | 90 | 5 | 0 |
| Boolector | 0 | 133 | 2330.755 | 2331.214 | 133 | 133 | 0 | 90 | 6 | 0 |
| 2018-Boolectorn | 0 | 132 | 142.195 | 142.213 | 132 | 132 | 0 | 91 | 0 | 0 |
| Z3n | 0 | 132 | 2540.217 | 2539.375 | 132 | 132 | 0 | 91 | 25 | 0 |
| CVC4 | 0 | 132 | 2794.044 | 2791.496 | 132 | 132 | 0 | 91 | 10 | 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 | 87 | 18977.647 | 18978.739 | 87 | 0 | 87 | 136 | 3 | 0 |
| Poolector | 0 | 85 | 56967.938 | 23355.13 | 85 | 0 | 85 | 138 | 5 | 0 |
| Boolector | 0 | 84 | 23144.741 | 23145.76 | 84 | 0 | 84 | 139 | 6 | 0 |
| 2018-Boolectorn | 0 | 81 | 1897.758 | 1898.061 | 81 | 0 | 81 | 142 | 0 | 0 |
| CVC4 | 0 | 81 | 27788.282 | 27727.731 | 81 | 0 | 81 | 142 | 10 | 0 |
| Z3n | 0 | 66 | 63764.804 | 63765.542 | 66 | 0 | 66 | 157 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Boolectorn | 0 | 198 | 696.776 | 696.869 | 198 | 132 | 66 | 25 | 15 | 0 | |
| Yices 2.6.2 | 0 | 194 | 787.632 | 787.64 | 194 | 132 | 62 | 29 | 29 | 0 | |
| Boolector | 0 | 193 | 1023.545 | 1023.602 | 193 | 130 | 63 | 30 | 30 | 0 | |
| Poolector | 0 | 189 | 1778.455 | 1086.55 | 189 | 130 | 59 | 34 | 34 | 0 | |
| CVC4 | 0 | 188 | 1384.395 | 1379.88 | 188 | 132 | 56 | 35 | 35 | 0 | |
| Z3n | 0 | 182 | 1121.123 | 1120.285 | 182 | 131 | 51 | 41 | 41 | 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.