The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_BV division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 6861 Time Limit: 2400 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 | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 6731 | 275993.743 | 275774.048 | 6731 | 2529 | 4202 | 130 | 130 | 0 |
| Bitwuzla | 0 | 6730 | 276330.543 | 276081.508 | 6730 | 2528 | 4202 | 131 | 131 | 0 |
| Yices2-fixedn | 0 | 6719 | 284360.319 | 284020.362 | 6719 | 2520 | 4199 | 142 | 142 | 0 |
| 2019-Boolectorn | 0 | 6710 | 310012.216 | 309792.327 | 6710 | 2523 | 4187 | 151 | 151 | 0 |
| 2019-Poolectorn | 0 | 6681 | 727582.895 | 507512.197 | 6681 | 2501 | 4180 | 180 | 180 | 0 |
| STP + CMS | 0 | 6663 | 800836.498 | 540888.672 | 6663 | 2485 | 4178 | 198 | 190 | 0 |
| MinkeyRink-fixedn | 0 | 6660 | 728614.521 | 536647.352 | 6660 | 2514 | 4146 | 201 | 194 | 0 |
| CVC4 | 0 | 6329 | 915193.32 | 914747.172 | 6329 | 2477 | 3852 | 532 | 526 | 3 |
| MathSAT5n | 0 | 5967 | 1388776.927 | 1388625.6 | 5967 | 2192 | 3775 | 894 | 893 | 0 |
| z3n | 0 | 5905 | 1544654.899 | 1544550.544 | 5905 | 2341 | 3564 | 956 | 956 | 0 |
| LazyBV2Int | 0 | 3248 | 4598369.148 | 4598847.543 | 3248 | 561 | 2687 | 3613 | 3612 | 2 |
| MinkeyRink | 0 | 2120 | 9364.511 | 9311.779 | 2120 | 11 | 2109 | 4741 | 0 | 0 |
| STP + MergeSAT | 2 | 6633 | 439361.342 | 439592.858 | 6633 | 2459 | 4174 | 228 | 224 | 0 |
| Yices2 | 32 | 6578 | 402042.882 | 401890.737 | 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 | 6731 | 275993.743 | 275774.048 | 6731 | 2529 | 4202 | 130 | 130 | 0 |
| Bitwuzla | 0 | 6730 | 276330.543 | 276081.508 | 6730 | 2528 | 4202 | 131 | 131 | 0 |
| 2019-Poolectorn | 0 | 6721 | 1098730.745 | 278453.648 | 6721 | 2524 | 4197 | 140 | 140 | 0 |
| Yices2-fixedn | 0 | 6719 | 284360.319 | 284020.362 | 6719 | 2520 | 4199 | 142 | 142 | 0 |
| 2019-Boolectorn | 0 | 6710 | 310012.216 | 309792.327 | 6710 | 2523 | 4187 | 151 | 151 | 0 |
| MinkeyRink-fixedn | 0 | 6690 | 1138512.691 | 294436.103 | 6690 | 2528 | 4162 | 171 | 164 | 0 |
| STP + CMS | 0 | 6689 | 1177048.158 | 319019.61 | 6689 | 2503 | 4186 | 172 | 164 | 0 |
| CVC4 | 0 | 6329 | 915193.32 | 914747.172 | 6329 | 2477 | 3852 | 532 | 526 | 3 |
| MathSAT5n | 0 | 5967 | 1388776.927 | 1388625.6 | 5967 | 2192 | 3775 | 894 | 893 | 0 |
| z3n | 0 | 5905 | 1544654.899 | 1544550.544 | 5905 | 2341 | 3564 | 956 | 956 | 0 |
| LazyBV2Int | 0 | 3248 | 4598369.148 | 4598847.543 | 3248 | 561 | 2687 | 3613 | 3612 | 2 |
| MinkeyRink | 0 | 2120 | 9364.511 | 9311.779 | 2120 | 11 | 2109 | 4741 | 0 | 0 |
| STP + MergeSAT | 2 | 6633 | 439361.342 | 439592.858 | 6633 | 2459 | 4174 | 228 | 224 | 0 |
| Yices2 | 32 | 6578 | 402042.882 | 401890.737 | 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 | 102586.329 | 102423.331 | 2529 | 2529 | 0 | 4332 | 130 | 0 |
| MinkeyRink-fixedn | 0 | 2528 | 331817.09 | 88955.153 | 2528 | 2528 | 0 | 4333 | 164 | 0 |
| Bitwuzla | 0 | 2528 | 102844.804 | 102707.819 | 2528 | 2528 | 0 | 4333 | 131 | 0 |
| 2019-Poolectorn | 0 | 2524 | 416559.082 | 105531.752 | 2524 | 2524 | 0 | 4337 | 140 | 0 |
| 2019-Boolectorn | 0 | 2523 | 116823.664 | 116660.861 | 2523 | 2523 | 0 | 4338 | 151 | 0 |
| Yices2-fixedn | 0 | 2520 | 108984.127 | 108754.99 | 2520 | 2520 | 0 | 4341 | 142 | 0 |
| STP + CMS | 0 | 2503 | 489347.036 | 141326.743 | 2503 | 2503 | 0 | 4358 | 164 | 0 |
| CVC4 | 0 | 2477 | 224790.536 | 224530.396 | 2477 | 2477 | 0 | 4384 | 526 | 3 |
| STP + MergeSAT | 0 | 2459 | 203925.735 | 204387.666 | 2459 | 2459 | 0 | 4402 | 224 | 0 |
| z3n | 0 | 2341 | 491335.154 | 491323.472 | 2341 | 2341 | 0 | 4520 | 956 | 0 |
| MathSAT5n | 0 | 2192 | 604559.231 | 604409.469 | 2192 | 2192 | 0 | 4669 | 893 | 0 |
| LazyBV2Int | 0 | 561 | 2573457.864 | 2573774.886 | 561 | 561 | 0 | 6300 | 3612 | 2 |
| MinkeyRink | 0 | 11 | 7036.84 | 6987.732 | 11 | 11 | 0 | 6850 | 0 | 0 |
| Yices2 | 32 | 2398 | 207399.001 | 207346.015 | 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 | 127811.964 | 127748.917 | 4202 | 0 | 4202 | 2659 | 130 | 0 |
| Bitwuzla | 0 | 4202 | 127889.219 | 127771.778 | 4202 | 0 | 4202 | 2659 | 131 | 0 |
| Yices2-fixedn | 0 | 4199 | 129779.002 | 129663.672 | 4199 | 0 | 4199 | 2662 | 142 | 0 |
| 2019-Poolectorn | 0 | 4197 | 502162.274 | 127318.776 | 4197 | 0 | 4197 | 2664 | 140 | 0 |
| 2019-Boolectorn | 0 | 4187 | 147593.432 | 147529.866 | 4187 | 0 | 4187 | 2674 | 151 | 0 |
| STP + CMS | 0 | 4186 | 507934.121 | 132090.847 | 4186 | 0 | 4186 | 2675 | 164 | 0 |
| Yices2 | 0 | 4180 | 149047.291 | 148943.202 | 4180 | 0 | 4180 | 2681 | 251 | 0 |
| MinkeyRink-fixedn | 0 | 4162 | 626798.431 | 159878.87 | 4162 | 0 | 4162 | 2699 | 164 | 0 |
| CVC4 | 0 | 3852 | 644809.124 | 644614.636 | 3852 | 0 | 3852 | 3009 | 526 | 3 |
| MathSAT5n | 0 | 3775 | 738625.406 | 738614.271 | 3775 | 0 | 3775 | 3086 | 893 | 0 |
| z3n | 0 | 3564 | 1007724.985 | 1007624.952 | 3564 | 0 | 3564 | 3297 | 956 | 0 |
| LazyBV2Int | 0 | 2687 | 1979315.643 | 1979470.816 | 2687 | 0 | 2687 | 4174 | 3612 | 2 |
| MinkeyRink | 0 | 2109 | 1918.408 | 1914.527 | 2109 | 0 | 2109 | 4752 | 0 | 0 |
| STP + MergeSAT | 2 | 4174 | 189839.827 | 189603.943 | 4174 | 0 | 4174 | 2687 | 224 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | 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.