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 Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 7538 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Boolector | Par4 | Poolector | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Boolector | 0 | 7520 | 63909.807 | 63883.284 | 7520 | 5160 | 2360 | 18 | 18 | 0 | |
| Par4 | 0 | 7518 | 66599.68 | 54472.46 | 7518 | 5159 | 2359 | 20 | 20 | 0 | |
| 2018-Boolectorn | 0 | 7515 | 76014.897 | 75990.654 | 7515 | 5155 | 2360 | 23 | 23 | 0 | |
| Yices 2.6.2 | 0 | 7512 | 93508.913 | 93548.847 | 7512 | 5158 | 2354 | 26 | 26 | 0 | |
| Poolector | 0 | 7512 | 99131.528 | 72714.133 | 7512 | 5159 | 2353 | 26 | 26 | 0 | |
| CVC4 | 0 | 7458 | 205434.874 | 207621.343 | 7458 | 5136 | 2322 | 80 | 80 | 0 | |
| Z3n | 0 | 7455 | 229875.125 | 229878.689 | 7455 | 5130 | 2325 | 83 | 83 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 7520 | 68137.25 | 51792.261 | 7520 | 5159 | 2361 | 18 | 18 | 0 | |
| Poolector | 0 | 7520 | 111313.528 | 61433.34 | 7520 | 5160 | 2360 | 18 | 18 | 0 | |
| Boolector | 0 | 7520 | 63913.337 | 63882.444 | 7520 | 5160 | 2360 | 18 | 18 | 0 | |
| 2018-Boolectorn | 0 | 7515 | 76019.587 | 75989.774 | 7515 | 5155 | 2360 | 23 | 23 | 0 | |
| Yices 2.6.2 | 0 | 7512 | 93513.613 | 93547.697 | 7512 | 5158 | 2354 | 26 | 26 | 0 | |
| CVC4 | 0 | 7458 | 207477.384 | 207617.383 | 7458 | 5136 | 2322 | 80 | 80 | 0 | |
| Z3n | 0 | 7455 | 229893.035 | 229875.199 | 7455 | 5130 | 2325 | 83 | 83 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Poolector | 0 | 5160 | 15716.984 | 4678.765 | 5160 | 5160 | 0 | 2378 | 18 | 0 |
| Boolector | 0 | 5160 | 10128.291 | 10098.744 | 5160 | 5160 | 0 | 2378 | 18 | 0 |
| Par4 | 0 | 5159 | 9951.011 | 5110.068 | 5159 | 5159 | 0 | 2379 | 18 | 0 |
| Yices 2.6.2 | 0 | 5158 | 16487.626 | 16508.882 | 5158 | 5158 | 0 | 2380 | 26 | 0 |
| 2018-Boolectorn | 0 | 5155 | 20655.984 | 20628.543 | 5155 | 5155 | 0 | 2383 | 23 | 0 |
| CVC4 | 0 | 5136 | 66042.951 | 66180.52 | 5136 | 5136 | 0 | 2402 | 80 | 0 |
| Z3n | 0 | 5130 | 81866.505 | 81860.238 | 5130 | 5130 | 0 | 2408 | 83 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 2361 | 58186.24 | 46682.193 | 2361 | 0 | 2361 | 5177 | 18 | 0 |
| Boolector | 0 | 2360 | 53785.046 | 53783.7 | 2360 | 0 | 2360 | 5178 | 18 | 0 |
| 2018-Boolectorn | 0 | 2360 | 55363.603 | 55361.231 | 2360 | 0 | 2360 | 5178 | 23 | 0 |
| Poolector | 0 | 2360 | 95596.545 | 56754.575 | 2360 | 0 | 2360 | 5178 | 18 | 0 |
| Yices 2.6.2 | 0 | 2354 | 77025.988 | 77038.815 | 2354 | 0 | 2354 | 5184 | 26 | 0 |
| Z3n | 0 | 2325 | 148026.53 | 148014.961 | 2325 | 0 | 2325 | 5213 | 83 | 0 |
| CVC4 | 0 | 2322 | 141434.432 | 141436.862 | 2322 | 0 | 2322 | 5216 | 80 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 7476 | 3757.63 | 2444.525 | 7476 | 5140 | 2336 | 62 | 62 | 0 | |
| Poolector | 0 | 7460 | 7054.415 | 4218.69 | 7460 | 5137 | 2323 | 78 | 78 | 0 | |
| Boolector | 0 | 7440 | 3736.126 | 3701.736 | 7440 | 5117 | 2323 | 98 | 98 | 0 | |
| Yices 2.6.2 | 0 | 7427 | 4123.537 | 4154.32 | 7427 | 5117 | 2310 | 111 | 111 | 0 | |
| 2018-Boolectorn | 0 | 7425 | 4872.715 | 4871.149 | 7425 | 5108 | 2317 | 113 | 113 | 0 | |
| CVC4 | 0 | 7392 | 6209.573 | 6191.473 | 7392 | 5098 | 2294 | 146 | 146 | 0 | |
| Z3n | 0 | 7344 | 6575.188 | 6553.871 | 7344 | 5064 | 2280 | 194 | 194 | 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.