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 2022-08-10 11:17:45 +0000
Benchmarks: 8464 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 | STP | STP |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| STP-fixedn | 0 | 8283 | 333501.284 | 333255.346 | 8283 | 3081 | 5202 | 181 | 0 | 180 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 8263 | 401954.5 | 401645.221 | 8263 | 3065 | 5198 | 201 | 0 | 201 | 0 |
| Bitwuzla | 0 | 8257 | 406914.731 | 406646.572 | 8257 | 3063 | 5194 | 207 | 0 | 207 | 0 |
| Yices2 | 0 | 8203 | 461381.627 | 461150.979 | 8203 | 3033 | 5170 | 261 | 0 | 262 | 0 |
| STP | 0 | 8196 | 446006.183 | 445818.377 | 8196 | 2992 | 5204 | 268 | 0 | 267 | 0 |
| cvc5 | 0 | 7707 | 1283097.616 | 1282497.621 | 7707 | 2929 | 4778 | 757 | 0 | 753 | 1 |
| Z3++BV | 0 | 7452 | 1489806.701 | 1489453.617 | 7452 | 2967 | 4485 | 1012 | 0 | 934 | 0 |
| MathSATn | 0 | 7230 | 1883174.644 | 1882708.237 | 7230 | 2619 | 4611 | 1234 | 0 | 1231 | 2 |
| z3-4.8.17n | 0 | 7203 | 1898996.517 | 1898940.396 | 7203 | 2808 | 4395 | 1261 | 0 | 1260 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| STP-fixedn | 0 | 8283 | 333523.644 | 333248.356 | 8283 | 3081 | 5202 | 181 | 0 | 180 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 8263 | 401982.76 | 401637.351 | 8263 | 3065 | 5198 | 201 | 0 | 201 | 0 |
| Bitwuzla | 0 | 8257 | 406943.741 | 406638.502 | 8257 | 3063 | 5194 | 207 | 0 | 207 | 0 |
| Yices2 | 0 | 8202 | 461404.797 | 461141.329 | 8202 | 3032 | 5170 | 262 | 0 | 262 | 0 |
| STP | 0 | 8196 | 446039.643 | 445808.697 | 8196 | 2992 | 5204 | 268 | 0 | 267 | 0 |
| cvc5 | 0 | 7707 | 1283258.326 | 1282463.871 | 7707 | 2929 | 4778 | 757 | 0 | 753 | 1 |
| Z3++BV | 0 | 7452 | 1489942.791 | 1489416.417 | 7452 | 2967 | 4485 | 1012 | 0 | 934 | 0 |
| MathSATn | 0 | 7230 | 1883449.514 | 1882652.087 | 7230 | 2619 | 4611 | 1234 | 0 | 1231 | 2 |
| z3-4.8.17n | 0 | 7203 | 1899207.857 | 1898887.656 | 7203 | 2808 | 4395 | 1261 | 0 | 1260 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| STP-fixedn | 0 | 3081 | 99340.344 | 99195.66 | 3081 | 3081 | 0 | 40 | 5343 | 180 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 3065 | 146171.271 | 146012.52 | 3065 | 3065 | 0 | 56 | 5343 | 201 | 0 |
| Bitwuzla | 0 | 3063 | 147030.947 | 146855.296 | 3063 | 3063 | 0 | 58 | 5343 | 207 | 0 |
| Yices2 | 0 | 3032 | 187620.322 | 187430.088 | 3032 | 3032 | 0 | 89 | 5343 | 262 | 0 |
| STP | 0 | 2992 | 211912.469 | 211831.56 | 2992 | 2992 | 0 | 129 | 5343 | 267 | 0 |
| Z3++BV | 0 | 2967 | 381961.932 | 381641.83 | 2967 | 2967 | 0 | 154 | 5343 | 934 | 0 |
| cvc5 | 0 | 2929 | 381320.164 | 380723.391 | 2929 | 2929 | 0 | 192 | 5343 | 753 | 1 |
| z3-4.8.17n | 0 | 2808 | 550946.041 | 550711.559 | 2808 | 2808 | 0 | 313 | 5343 | 1260 | 0 |
| MathSATn | 0 | 2619 | 797360.289 | 796853.774 | 2619 | 2619 | 0 | 502 | 5343 | 1231 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| STP | 0 | 5204 | 159727.174 | 159577.137 | 5204 | 0 | 5204 | 77 | 3183 | 267 | 0 |
| STP-fixedn | 0 | 5202 | 159783.301 | 159652.696 | 5202 | 0 | 5202 | 79 | 3183 | 180 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 5198 | 181411.489 | 181224.831 | 5198 | 0 | 5198 | 83 | 3183 | 201 | 0 |
| Bitwuzla | 0 | 5194 | 185512.794 | 185383.206 | 5194 | 0 | 5194 | 87 | 3183 | 207 | 0 |
| Yices2 | 0 | 5170 | 199384.476 | 199311.241 | 5170 | 0 | 5170 | 111 | 3183 | 262 | 0 |
| cvc5 | 0 | 4778 | 827538.162 | 827340.48 | 4778 | 0 | 4778 | 503 | 3183 | 753 | 1 |
| MathSATn | 0 | 4611 | 1011689.225 | 1011398.313 | 4611 | 0 | 4611 | 670 | 3183 | 1231 | 2 |
| Z3++BV | 0 | 4485 | 1033580.859 | 1033374.587 | 4485 | 0 | 4485 | 796 | 3183 | 934 | 0 |
| z3-4.8.17n | 0 | 4395 | 1273861.816 | 1273776.097 | 4395 | 0 | 4395 | 886 | 3183 | 1260 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| STP-fixedn | 0 | 7782 | 29005.815 | 28823.586 | 7782 | 2851 | 4931 | 682 | 0 | 681 | 0 |
| STP | 0 | 7627 | 31668.916 | 31511.761 | 7627 | 2705 | 4922 | 837 | 0 | 836 | 0 |
| Bitwuzla | 0 | 7573 | 43753.048 | 43452.271 | 7573 | 2734 | 4839 | 891 | 0 | 891 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 7553 | 43140.62 | 42864.416 | 7553 | 2706 | 4847 | 911 | 0 | 911 | 0 |
| Yices2 | 0 | 7480 | 33681.215 | 33541.763 | 7480 | 2568 | 4912 | 984 | 0 | 984 | 0 |
| Z3++BV | 0 | 6083 | 75232.23 | 74848.758 | 6083 | 2201 | 3882 | 2381 | 0 | 2305 | 0 |
| cvc5 | 0 | 5955 | 91114.339 | 90686.24 | 5955 | 1955 | 4000 | 2509 | 0 | 2508 | 1 |
| MathSATn | 0 | 5716 | 82967.541 | 82712.854 | 5716 | 1843 | 3873 | 2748 | 0 | 2745 | 2 |
| z3-4.8.17n | 0 | 5580 | 88020.048 | 87796.761 | 5580 | 1890 | 3690 | 2884 | 0 | 2884 | 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.