The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the BV division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 696 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-Par4n | 0 | 659 | 49658.532 | 45778.813 | 659 | 196 | 463 | 37 | 37 | 0 | |
| CVC4 | 0 | 612 | 135421.639 | 138922.161 | 612 | 167 | 445 | 84 | 84 | 0 | |
| Bitwuzla-fixedn | 0 | 595 | 132010.761 | 126665.336 | 595 | 191 | 404 | 101 | 101 | 0 | |
| z3n | 0 | 576 | 144196.574 | 144217.607 | 576 | 173 | 403 | 120 | 116 | 1 | |
| UltimateEliminator+MathSAT | 0 | 227 | 126646.048 | 125544.9 | 227 | 13 | 214 | 469 | 103 | 0 | |
| Bitwuzla | 40 | 569 | 108290.851 | 106379.013 | 569 | 183 | 386 | 127 | 87 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 663 | 54497.472 | 43423.935 | 663 | 198 | 465 | 33 | 33 | 0 | |
| CVC4 | 0 | 612 | 137860.739 | 138917.711 | 612 | 167 | 445 | 84 | 84 | 0 | |
| Bitwuzla-fixedn | 0 | 598 | 133286.041 | 125513.756 | 598 | 193 | 405 | 98 | 98 | 0 | |
| z3n | 0 | 576 | 144211.864 | 144213.127 | 576 | 173 | 403 | 120 | 116 | 1 | |
| UltimateEliminator+MathSAT | 0 | 227 | 126646.048 | 125544.9 | 227 | 13 | 214 | 469 | 103 | 0 | |
| Bitwuzla | 40 | 571 | 108452.381 | 105260.363 | 571 | 183 | 388 | 125 | 85 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 198 | 20522.286 | 14179.19 | 198 | 198 | 0 | 498 | 33 | 0 |
| Bitwuzla-fixedn | 0 | 193 | 25656.28 | 21863.603 | 193 | 193 | 0 | 503 | 98 | 0 |
| z3n | 0 | 173 | 39342.091 | 39342.39 | 173 | 173 | 0 | 523 | 116 | 1 |
| CVC4 | 0 | 167 | 82986.999 | 83940.926 | 167 | 167 | 0 | 529 | 84 | 0 |
| UltimateEliminator+MathSAT | 0 | 13 | 74566.073 | 73996.171 | 13 | 13 | 0 | 683 | 103 | 0 |
| Bitwuzla | 14 | 183 | 13745.374 | 13484.816 | 183 | 183 | 0 | 513 | 85 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 465 | 23175.186 | 18444.745 | 465 | 0 | 465 | 231 | 33 | 0 |
| CVC4 | 0 | 445 | 44073.741 | 44176.785 | 445 | 0 | 445 | 251 | 84 | 0 |
| Bitwuzla-fixedn | 0 | 405 | 96829.762 | 92850.154 | 405 | 0 | 405 | 291 | 98 | 0 |
| z3n | 0 | 403 | 94069.773 | 94070.737 | 403 | 0 | 403 | 293 | 116 | 1 |
| UltimateEliminator+MathSAT | 0 | 214 | 49652.688 | 49132.128 | 214 | 0 | 214 | 482 | 103 | 0 |
| Bitwuzla | 26 | 388 | 83907.007 | 80975.547 | 388 | 0 | 388 | 308 | 85 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 644 | 2652.822 | 1651.77 | 644 | 186 | 458 | 52 | 52 | 0 | |
| Bitwuzla-fixedn | 0 | 565 | 4088.43 | 3645.216 | 565 | 181 | 384 | 131 | 131 | 0 | |
| z3n | 0 | 559 | 3606.942 | 3607.062 | 559 | 171 | 388 | 137 | 136 | 1 | |
| CVC4 | 0 | 529 | 4660.844 | 4647.141 | 529 | 99 | 430 | 167 | 167 | 0 | |
| UltimateEliminator+MathSAT | 0 | 226 | 5009.976 | 4194.233 | 226 | 13 | 213 | 470 | 109 | 0 | |
| Bitwuzla | 40 | 552 | 3170.007 | 2858.553 | 552 | 181 | 371 | 144 | 104 | 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.