The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Bitvec division in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 8828 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Bitwuzla | Bitwuzla | Bitwuzla | Yices2 | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 8644 | 376556.809 | 376184.839 | 8644 | 3193 | 5451 | 184 | 0 | 184 | 0 |
| Bitwuzla | 0 | 8610 | 411621.368 | 411148.918 | 8610 | 3190 | 5420 | 218 | 0 | 218 | 0 |
| Yices2 | 0 | 8598 | 437056.235 | 436896.084 | 8598 | 3162 | 5436 | 230 | 0 | 230 | 0 |
| STP | 0 | 8425 | 789958.195 | 566343.343 | 8425 | 3067 | 5358 | 403 | 0 | 397 | 0 |
| cvc5 | 0 | 8135 | 1222789.394 | 1221961.05 | 8135 | 3085 | 5050 | 693 | 0 | 685 | 2 |
| MathSAT5n | 0 | 7645 | 1819478.575 | 1819168.857 | 7645 | 2775 | 4870 | 1183 | 0 | 1180 | 2 |
| z3n | 0 | 7406 | 2178189.207 | 2178343.083 | 7406 | 2920 | 4486 | 1422 | 0 | 1422 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 8644 | 376584.659 | 376178.339 | 8644 | 3193 | 5451 | 184 | 0 | 184 | 0 |
| Bitwuzla | 0 | 8610 | 411647.978 | 411141.768 | 8610 | 3190 | 5420 | 218 | 0 | 218 | 0 |
| Yices2 | 0 | 8598 | 437075.315 | 436889.514 | 8598 | 3162 | 5436 | 230 | 0 | 230 | 0 |
| STP | 0 | 8572 | 944672.975 | 475022.754 | 8572 | 3148 | 5424 | 256 | 0 | 250 | 0 |
| cvc5 | 0 | 8135 | 1222929.914 | 1221931.01 | 8135 | 3085 | 5050 | 693 | 0 | 685 | 2 |
| MathSAT5n | 0 | 7645 | 1820011.415 | 1819115.097 | 7645 | 2775 | 4870 | 1183 | 0 | 1180 | 2 |
| z3n | 0 | 7406 | 2178693.897 | 2178282.533 | 7406 | 2920 | 4486 | 1422 | 0 | 1422 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 3193 | 134450.495 | 134221.819 | 3193 | 3193 | 0 | 52 | 5583 | 184 | 0 |
| Bitwuzla | 0 | 3190 | 133244.928 | 133033.779 | 3190 | 3190 | 0 | 55 | 5583 | 218 | 0 |
| Yices2 | 0 | 3162 | 180483.722 | 180332.817 | 3162 | 3162 | 0 | 83 | 5583 | 230 | 0 |
| STP | 0 | 3148 | 461089.945 | 208185.981 | 3148 | 3148 | 0 | 97 | 5583 | 250 | 0 |
| cvc5 | 0 | 3085 | 358540.702 | 357804.214 | 3085 | 3085 | 0 | 160 | 5583 | 685 | 2 |
| z3n | 0 | 2920 | 679296.461 | 679104.285 | 2920 | 2920 | 0 | 325 | 5583 | 1422 | 0 |
| MathSAT5n | 0 | 2775 | 761625.044 | 760938.499 | 2775 | 2775 | 0 | 470 | 5583 | 1180 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 5451 | 185734.164 | 185556.521 | 5451 | 0 | 5451 | 85 | 3292 | 184 | 0 |
| Yices2 | 0 | 5436 | 200191.593 | 200156.697 | 5436 | 0 | 5436 | 100 | 3292 | 230 | 0 |
| STP | 0 | 5424 | 427183.03 | 210436.773 | 5424 | 0 | 5424 | 112 | 3292 | 250 | 0 |
| Bitwuzla | 0 | 5420 | 222003.05 | 221707.989 | 5420 | 0 | 5420 | 116 | 3292 | 218 | 0 |
| cvc5 | 0 | 5050 | 807989.212 | 807726.796 | 5050 | 0 | 5050 | 486 | 3292 | 685 | 2 |
| MathSAT5n | 0 | 4870 | 1001986.371 | 1001776.598 | 4870 | 0 | 4870 | 666 | 3292 | 1180 | 2 |
| z3n | 0 | 4486 | 1442997.436 | 1442778.248 | 4486 | 0 | 4486 | 1050 | 3292 | 1422 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 7926 | 43027.92 | 42742.551 | 7926 | 2852 | 5074 | 902 | 0 | 902 | 0 |
| Bitwuzla | 0 | 7909 | 43831.935 | 43515.235 | 7909 | 2843 | 5066 | 919 | 0 | 919 | 0 |
| Yices2 | 0 | 7883 | 33343.195 | 33253.704 | 7883 | 2723 | 5160 | 945 | 0 | 945 | 0 |
| STP | 0 | 7666 | 62996.229 | 41348.748 | 7666 | 2681 | 4985 | 1162 | 0 | 1161 | 0 |
| cvc5 | 0 | 6236 | 91507.333 | 90968.544 | 6236 | 1999 | 4237 | 2592 | 0 | 2590 | 2 |
| MathSAT5n | 0 | 6049 | 83742.918 | 83423.143 | 6049 | 2029 | 4020 | 2779 | 0 | 2776 | 2 |
| z3n | 0 | 5568 | 95207.061 | 94982.188 | 5568 | 1849 | 3719 | 3260 | 0 | 3260 | 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.