The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Bitvec division in the Single Query Track.
Page generated on 2021-07-18 17:29:05 +0000
Benchmarks: 970 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 891 | 104548.597 | 97375.374 | 891 | 231 | 660 | 79 | 0 | 79 | 0 |
| cvc5 | 0 | 808 | 199838.482 | 232187.057 | 808 | 181 | 627 | 162 | 0 | 162 | 0 |
| z3n | 0 | 786 | 217529.325 | 217615.944 | 786 | 205 | 581 | 184 | 0 | 172 | 1 |
| Yices2-QS | 0 | 715 | 310551.346 | 310569.131 | 715 | 174 | 541 | 255 | 0 | 251 | 0 |
| UltimateEliminator+MathSAT | 0 | 306 | 162589.399 | 159362.04 | 306 | 21 | 285 | 664 | 0 | 120 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 896 | 115714.117 | 94773.634 | 896 | 232 | 664 | 74 | 0 | 74 | 0 |
| cvc5 | 0 | 808 | 231940.284 | 232179.877 | 808 | 181 | 627 | 162 | 0 | 162 | 0 |
| z3n | 0 | 786 | 217605.375 | 217608.324 | 786 | 205 | 581 | 184 | 0 | 172 | 1 |
| Yices2-QS | 0 | 715 | 310593.266 | 310558.621 | 715 | 174 | 541 | 255 | 0 | 251 | 0 |
| UltimateEliminator+MathSAT | 0 | 306 | 162589.399 | 159362.04 | 306 | 21 | 285 | 664 | 0 | 120 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 232 | 25298.228 | 17174.31 | 232 | 232 | 0 | 13 | 725 | 74 | 0 |
| z3n | 0 | 205 | 44229.874 | 44231.007 | 205 | 205 | 0 | 40 | 725 | 172 | 1 |
| cvc5 | 0 | 181 | 108317.892 | 108537.226 | 181 | 181 | 0 | 64 | 725 | 162 | 0 |
| Yices2-QS | 0 | 174 | 85034.356 | 85034.833 | 174 | 174 | 0 | 71 | 725 | 251 | 0 |
| UltimateEliminator+MathSAT | 0 | 21 | 90859.735 | 89597.294 | 21 | 21 | 0 | 224 | 725 | 120 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 664 | 58015.889 | 45199.324 | 664 | 0 | 664 | 34 | 272 | 74 | 0 |
| cvc5 | 0 | 627 | 91222.391 | 91242.651 | 627 | 0 | 627 | 71 | 272 | 162 | 0 |
| z3n | 0 | 581 | 141870.194 | 141871.739 | 581 | 0 | 581 | 117 | 272 | 172 | 1 |
| Yices2-QS | 0 | 541 | 193158.91 | 193123.788 | 541 | 0 | 541 | 157 | 272 | 251 | 0 |
| UltimateEliminator+MathSAT | 0 | 285 | 54828.366 | 52978.264 | 285 | 0 | 285 | 413 | 272 | 120 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 870 | 4480.951 | 2999.086 | 870 | 223 | 647 | 100 | 0 | 100 | 0 |
| z3n | 0 | 758 | 5606.426 | 5606.893 | 758 | 197 | 561 | 212 | 0 | 211 | 1 |
| cvc5 | 0 | 715 | 6952.058 | 6941.51 | 715 | 122 | 593 | 255 | 0 | 255 | 0 |
| Yices2-QS | 0 | 689 | 7062.602 | 7050.744 | 689 | 166 | 523 | 281 | 0 | 279 | 0 |
| UltimateEliminator+MathSAT | 0 | 288 | 9189.421 | 7311.011 | 288 | 12 | 276 | 682 | 0 | 170 | 1 |
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.