The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the BVFP division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 224 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 181 | 33976.556 | 33925.24 | 181 | 169 | 12 | 43 | 24 | 0 | |
| CVC4 | 0 | 113 | 38475.375 | 38480.586 | 113 | 109 | 4 | 111 | 32 | 0 | |
| UltimateEliminator+MathSAT | 0 | 27 | 1978.266 | 1731.256 | 27 | 23 | 4 | 197 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 181 | 33982.226 | 33924.06 | 181 | 169 | 12 | 43 | 24 | 0 | |
| CVC4 | 0 | 113 | 38479.305 | 38479.356 | 113 | 109 | 4 | 111 | 32 | 0 | |
| UltimateEliminator+MathSAT | 0 | 27 | 1978.266 | 1731.256 | 27 | 23 | 4 | 197 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 169 | 22430.837 | 22430.003 | 169 | 169 | 0 | 55 | 24 | 0 |
| CVC4 | 0 | 109 | 34834.837 | 34834.797 | 109 | 109 | 0 | 115 | 32 | 0 |
| UltimateEliminator+MathSAT | 0 | 23 | 660.79 | 450.771 | 23 | 23 | 0 | 201 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 12 | 401.902 | 401.931 | 12 | 0 | 12 | 212 | 24 | 0 |
| CVC4 | 0 | 4 | 4.888 | 4.885 | 4 | 0 | 4 | 220 | 32 | 0 |
| UltimateEliminator+MathSAT | 0 | 4 | 44.144 | 30.354 | 4 | 0 | 4 | 220 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 155 | 1797.934 | 1796.477 | 155 | 146 | 9 | 69 | 56 | 0 | |
| CVC4 | 0 | 113 | 847.305 | 847.356 | 113 | 109 | 4 | 111 | 32 | 0 | |
| UltimateEliminator+MathSAT | 0 | 27 | 802.266 | 555.256 | 27 | 23 | 4 | 197 | 1 | 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.