The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BV division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 6861 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 6731 | 275993.133 | 275773.208 | 6731 | 2529 | 4202 | 130 | 130 | 0 | |
| Bitwuzla | 0 | 6730 | 276329.653 | 276080.188 | 6730 | 2528 | 4202 | 131 | 131 | 0 | |
| Yices2-fixedn | 0 | 6719 | 284359.239 | 284018.222 | 6719 | 2520 | 4199 | 142 | 142 | 0 | |
| 2019-Boolectorn | 0 | 6710 | 310011.466 | 309790.697 | 6710 | 2523 | 4187 | 151 | 151 | 0 | |
| 2019-Poolectorn | 0 | 6632 | 484753.535 | 328685.732 | 6632 | 2477 | 4155 | 229 | 229 | 0 | |
| MinkeyRink-fixedn | 0 | 6610 | 470014.391 | 341671.944 | 6610 | 2488 | 4122 | 251 | 244 | 0 | |
| STP + CMS | 0 | 6580 | 546415.328 | 391932.497 | 6580 | 2423 | 4157 | 281 | 273 | 0 | |
| CVC4 | 0 | 6329 | 911591.33 | 911144.212 | 6329 | 2477 | 3852 | 532 | 526 | 3 | |
| MathSAT5n | 0 | 5967 | 1388776.257 | 1388624.33 | 5967 | 2192 | 3775 | 894 | 893 | 0 | |
| z3n | 0 | 5905 | 1544650.759 | 1544542.384 | 5905 | 2341 | 3564 | 956 | 956 | 0 | |
| LazyBV2Int | 0 | 3248 | 4595944.878 | 4596409.433 | 3248 | 561 | 2687 | 3613 | 3612 | 2 | |
| MinkeyRink | 0 | 2120 | 9364.511 | 9311.779 | 2120 | 11 | 2109 | 4741 | 0 | 0 | |
| STP + MergeSAT | 2 | 6633 | 439359.742 | 439590.458 | 6633 | 2459 | 4174 | 228 | 224 | 0 | |
| Yices2 | 32 | 6578 | 402038.802 | 401885.717 | 6578 | 2398 | 4180 | 283 | 251 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 6731 | 276009.913 | 275768.178 | 6731 | 2529 | 4202 | 130 | 130 | 0 | |
| Bitwuzla | 0 | 6730 | 276345.813 | 276075.568 | 6730 | 2528 | 4202 | 131 | 131 | 0 | |
| 2019-Poolectorn | 0 | 6721 | 601905.825 | 278442.308 | 6721 | 2524 | 4197 | 140 | 140 | 0 | |
| Yices2-fixedn | 0 | 6719 | 284373.409 | 284013.912 | 6719 | 2520 | 4199 | 142 | 142 | 0 | |
| 2019-Boolectorn | 0 | 6710 | 310030.086 | 309784.927 | 6710 | 2523 | 4187 | 151 | 151 | 0 | |
| MinkeyRink-fixedn | 0 | 6690 | 561747.841 | 294426.483 | 6690 | 2528 | 4162 | 171 | 164 | 0 | |
| STP + CMS | 0 | 6689 | 642484.468 | 319011.01 | 6689 | 2503 | 4186 | 172 | 164 | 0 | |
| CVC4 | 0 | 6329 | 911688.83 | 911121.552 | 6329 | 2477 | 3852 | 532 | 526 | 3 | |
| MathSAT5n | 0 | 5967 | 1388964.657 | 1388584.66 | 5967 | 2192 | 3775 | 894 | 893 | 0 | |
| z3n | 0 | 5905 | 1544785.719 | 1544502.874 | 5905 | 2341 | 3564 | 956 | 956 | 0 | |
| LazyBV2Int | 0 | 3247 | 4596373.638 | 4596276.613 | 3247 | 560 | 2687 | 3614 | 3612 | 2 | |
| MinkeyRink | 0 | 2120 | 9364.511 | 9311.779 | 2120 | 11 | 2109 | 4741 | 0 | 0 | |
| STP + MergeSAT | 2 | 6633 | 439386.662 | 439583.558 | 6633 | 2459 | 4174 | 228 | 224 | 0 | |
| Yices2 | 32 | 6578 | 402053.912 | 401879.167 | 6578 | 2398 | 4180 | 283 | 251 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 2529 | 102591.669 | 102421.821 | 2529 | 2529 | 0 | 4332 | 130 | 0 |
| MinkeyRink-fixedn | 0 | 2528 | 224141.6 | 88953.453 | 2528 | 2528 | 0 | 4333 | 164 | 0 |
| Bitwuzla | 0 | 2528 | 102851.034 | 102706.249 | 2528 | 2528 | 0 | 4333 | 131 | 0 |
| 2019-Poolectorn | 0 | 2524 | 285094.752 | 105528.672 | 2524 | 2524 | 0 | 4337 | 140 | 0 |
| 2019-Boolectorn | 0 | 2523 | 116830.844 | 116658.891 | 2523 | 2523 | 0 | 4338 | 151 | 0 |
| Yices2-fixedn | 0 | 2520 | 108990.017 | 108753.1 | 2520 | 2520 | 0 | 4341 | 142 | 0 |
| STP + CMS | 0 | 2503 | 341801.786 | 141324.133 | 2503 | 2503 | 0 | 4358 | 164 | 0 |
| CVC4 | 0 | 2477 | 221216.036 | 220926.566 | 2477 | 2477 | 0 | 4384 | 526 | 3 |
| STP + MergeSAT | 0 | 2459 | 203940.205 | 204383.186 | 2459 | 2459 | 0 | 4402 | 224 | 0 |
| z3n | 0 | 2341 | 491381.274 | 491312.492 | 2341 | 2341 | 0 | 4520 | 956 | 0 |
| MathSAT5n | 0 | 2192 | 604638.661 | 604392.119 | 2192 | 2192 | 0 | 4669 | 893 | 0 |
| LazyBV2Int | 0 | 560 | 2573664.914 | 2573681.176 | 560 | 560 | 0 | 6301 | 3612 | 2 |
| MinkeyRink | 0 | 11 | 7036.84 | 6987.732 | 11 | 11 | 0 | 6850 | 0 | 0 |
| Yices2 | 32 | 2398 | 207402.541 | 207339.825 | 2398 | 2398 | 0 | 4463 | 251 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 4202 | 127818.244 | 127746.357 | 4202 | 0 | 4202 | 2659 | 130 | 0 |
| Bitwuzla | 0 | 4202 | 127894.779 | 127769.318 | 4202 | 0 | 4202 | 2659 | 131 | 0 |
| Yices2-fixedn | 0 | 4199 | 129783.392 | 129660.812 | 4199 | 0 | 4199 | 2662 | 142 | 0 |
| 2019-Poolectorn | 0 | 4197 | 271211.074 | 127313.636 | 4197 | 0 | 4197 | 2664 | 140 | 0 |
| 2019-Boolectorn | 0 | 4187 | 147599.242 | 147526.036 | 4187 | 0 | 4187 | 2674 | 151 | 0 |
| STP + CMS | 0 | 4186 | 255082.681 | 132086.877 | 4186 | 0 | 4186 | 2675 | 164 | 0 |
| Yices2 | 0 | 4180 | 149051.371 | 148939.342 | 4180 | 0 | 4180 | 2681 | 251 | 0 |
| MinkeyRink-fixedn | 0 | 4162 | 292006.241 | 159873.03 | 4162 | 0 | 4162 | 2699 | 164 | 0 |
| CVC4 | 0 | 3852 | 644872.794 | 644594.986 | 3852 | 0 | 3852 | 3009 | 526 | 3 |
| MathSAT5n | 0 | 3775 | 738725.996 | 738592.541 | 3775 | 0 | 3775 | 3086 | 893 | 0 |
| z3n | 0 | 3564 | 1007804.445 | 1007590.382 | 3564 | 0 | 3564 | 3297 | 956 | 0 |
| LazyBV2Int | 0 | 2687 | 1977108.723 | 1976995.436 | 2687 | 0 | 2687 | 4174 | 3612 | 2 |
| MinkeyRink | 0 | 2109 | 1918.408 | 1914.527 | 2109 | 0 | 2109 | 4752 | 0 | 0 |
| STP + MergeSAT | 2 | 4174 | 189846.457 | 189600.373 | 4174 | 0 | 4174 | 2687 | 224 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Poolectorn | 0 | 6211 | 72668.191 | 30874.689 | 6211 | 2246 | 3965 | 650 | 650 | 0 | |
| MinkeyRink-fixedn | 0 | 6201 | 42927.466 | 25104.899 | 6201 | 2255 | 3946 | 660 | 660 | 0 | |
| Bitwuzla | 0 | 6190 | 32777.904 | 32530.517 | 6190 | 2230 | 3960 | 671 | 671 | 0 | |
| Bitwuzla-fixedn | 0 | 6190 | 32790.103 | 32597.973 | 6190 | 2229 | 3961 | 671 | 671 | 0 | |
| Yices2-fixedn | 0 | 6182 | 24605.956 | 24517.889 | 6182 | 2168 | 4014 | 679 | 679 | 0 | |
| 2019-Boolectorn | 0 | 6181 | 31794.444 | 31669.739 | 6181 | 2223 | 3958 | 680 | 680 | 0 | |
| STP + CMS | 0 | 6082 | 45870.656 | 29734.296 | 6082 | 2149 | 3933 | 779 | 779 | 0 | |
| STP + MergeSAT | 0 | 5967 | 38364.565 | 38117.104 | 5967 | 2139 | 3828 | 894 | 894 | 0 | |
| CVC4 | 0 | 5005 | 68528.063 | 68179.957 | 5005 | 1727 | 3278 | 1856 | 1853 | 3 | |
| MathSAT5n | 0 | 4873 | 60047.395 | 59892.886 | 4873 | 1552 | 3321 | 1988 | 1988 | 0 | |
| z3n | 0 | 4448 | 72205.017 | 71999.22 | 4448 | 1487 | 2961 | 2413 | 2413 | 0 | |
| LazyBV2Int | 0 | 2323 | 113185.778 | 113123.074 | 2323 | 164 | 2159 | 4538 | 4536 | 2 | |
| MinkeyRink | 0 | 2120 | 5852.929 | 5799.139 | 2120 | 11 | 2109 | 4741 | 37 | 0 | |
| Yices2 | 32 | 6089 | 25474.635 | 25380.35 | 6089 | 2084 | 4005 | 772 | 740 | 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.