The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_FP division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 270 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla | COLIBRI |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 233 | 64601.558 | 64608.458 | 233 | 135 | 98 | 37 | 37 | 0 | |
| Bitwuzla | 0 | 233 | 64757.415 | 64716.937 | 233 | 135 | 98 | 37 | 37 | 0 | |
| 2019-Par4n | 0 | 218 | 73823.401 | 66246.872 | 218 | 120 | 98 | 52 | 52 | 0 | |
| COLIBRI | 0 | 214 | 68905.01 | 68911.515 | 214 | 117 | 97 | 56 | 56 | 0 | |
| MathSAT5n | 0 | 202 | 98436.622 | 98404.631 | 202 | 124 | 78 | 68 | 68 | 0 | |
| CVC4 | 0 | 202 | 105364.237 | 105382.294 | 202 | 119 | 83 | 68 | 68 | 0 | |
| z3n | 0 | 164 | 152777.619 | 152807.358 | 164 | 102 | 62 | 106 | 104 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 233 | 64606.818 | 64607.058 | 233 | 135 | 98 | 37 | 37 | 0 | |
| Bitwuzla | 0 | 233 | 64761.195 | 64715.517 | 233 | 135 | 98 | 37 | 37 | 0 | |
| 2019-Par4n | 0 | 224 | 81582.771 | 64035.242 | 224 | 125 | 99 | 46 | 46 | 0 | |
| COLIBRI | 0 | 214 | 68909.06 | 68909.645 | 214 | 117 | 97 | 56 | 56 | 0 | |
| MathSAT5n | 0 | 202 | 98448.712 | 98401.301 | 202 | 124 | 78 | 68 | 68 | 0 | |
| CVC4 | 0 | 202 | 105375.917 | 105379.464 | 202 | 119 | 83 | 68 | 68 | 0 | |
| z3n | 0 | 164 | 152798.749 | 152802.638 | 164 | 102 | 62 | 106 | 104 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 135 | 13539.167 | 13539.207 | 135 | 135 | 0 | 135 | 37 | 0 |
| Bitwuzla-fixedn | 0 | 135 | 13545.55 | 13546.833 | 135 | 135 | 0 | 135 | 37 | 0 |
| 2019-Par4n | 0 | 125 | 36530.943 | 24995.623 | 125 | 125 | 0 | 145 | 46 | 0 |
| MathSAT5n | 0 | 124 | 27252.366 | 27229.387 | 124 | 124 | 0 | 146 | 68 | 0 |
| CVC4 | 0 | 119 | 36828.685 | 36830.436 | 119 | 119 | 0 | 151 | 68 | 0 |
| COLIBRI | 0 | 117 | 29723.275 | 29723.662 | 117 | 117 | 0 | 153 | 56 | 0 |
| z3n | 0 | 102 | 63539.433 | 63542.19 | 102 | 102 | 0 | 168 | 104 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 99 | 29451.828 | 23439.619 | 99 | 0 | 99 | 171 | 46 | 0 |
| Bitwuzla-fixedn | 0 | 98 | 35461.268 | 35460.225 | 98 | 0 | 98 | 172 | 37 | 0 |
| Bitwuzla | 0 | 98 | 35622.029 | 35576.311 | 98 | 0 | 98 | 172 | 37 | 0 |
| COLIBRI | 0 | 97 | 23585.785 | 23585.984 | 97 | 0 | 97 | 173 | 56 | 0 |
| CVC4 | 0 | 83 | 52947.232 | 52949.028 | 83 | 0 | 83 | 187 | 68 | 0 |
| MathSAT5n | 0 | 78 | 55596.346 | 55571.914 | 78 | 0 | 78 | 192 | 68 | 0 |
| z3n | 0 | 62 | 73659.316 | 73660.448 | 62 | 0 | 62 | 208 | 104 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 195 | 2231.049 | 2231.535 | 195 | 111 | 84 | 75 | 75 | 0 | |
| 2019-Par4n | 0 | 186 | 3051.684 | 2397.193 | 186 | 102 | 84 | 84 | 84 | 0 | |
| Bitwuzla | 0 | 165 | 3030.418 | 3017.422 | 165 | 102 | 63 | 105 | 105 | 0 | |
| Bitwuzla-fixedn | 0 | 165 | 3022.373 | 3018.51 | 165 | 102 | 63 | 105 | 105 | 0 | |
| CVC4 | 0 | 124 | 4100.027 | 4100.07 | 124 | 75 | 49 | 146 | 146 | 0 | |
| MathSAT5n | 0 | 122 | 4276.25 | 4249.694 | 122 | 77 | 45 | 148 | 148 | 0 | |
| z3n | 0 | 60 | 5490.981 | 5491.01 | 60 | 39 | 21 | 210 | 208 | 2 |
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.