The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BV division as of Thu Jul 7 07:24:34 GMT
Benchmarks in this division: 26414
Time Limit: 1200s
| Sequential Performance | Parallel Performance |
|---|---|
| Boolector (preprop) | Boolector (preprop) |
| Solver | Error Score | Correct Score | avg. CPU time |
|---|---|---|---|
| Boolector (preprop) | 0.000 | 24473.995 | 266.928 |
| Boolector | 0.000 | 24468.395 | 265.950 |
| stp-cms-st | 0.000 | 24165.007 | 287.851 |
| z3n | 0.000 | 23729.054 | 333.506 |
| stp-cms-exp | 0.000 | 23640.669 | 307.450 |
| CVC4 | 0.000 | 23469.029 | 360.463 |
| Minkeyrink | 0.000 | 23444.824 | 363.504 |
| stp-cms-mt | 0.000 | 23440.401 | 357.733 |
| ABC_glucose | 0.000 | 23078.931 | 326.097 |
| Yices2 | 0.000 | 22687.777 | 435.806 |
| MathSat5n | 0.000 | 22496.779 | 444.780 |
| MapleSTP | 0.000 | 21764.885 | 524.588 |
| MapleSTP-mt | 0.000 | 21214.679 | 602.984 |
| stp-minisat-st | 0.000 | 20582.614 | 633.974 |
| ABC_default | 0.000 | 18528.788 | 477.649 |
| Q3B | 699.800 | 10325.715 | 1398.216 |
| Solver | Error Score | Correct Score | avg. CPU time | avg. WALL time | Unsolved |
|---|---|---|---|---|---|
| Boolector (preprop) | 0.000 | 24473.995 | 267.033 | 266.724 | 149 |
| Boolector | 0.000 | 24468.395 | 266.054 | 265.847 | 150 |
| Minkeyrink | 0.000 | 24434.194 | 907.913 | 244.071 | 193 |
| stp-cms-mt | 0.000 | 24244.599 | 865.550 | 249.079 | 216 |
| stp-cms-st | 0.000 | 24165.007 | 287.966 | 287.770 | 214 |
| CVC4 | 0.000 | 23820.707 | 583.314 | 291.599 | 231 |
| z3n | 0.000 | 23732.215 | 333.644 | 333.367 | 304 |
| stp-cms-exp | 0.000 | 23640.669 | 307.572 | 307.388 | 270 |
| ABC_glucose | 0.000 | 23078.931 | 326.388 | 326.028 | 477 |
| Yices2 | 0.000 | 22687.777 | 436.006 | 435.702 | 638 |
| MathSat5n | 0.000 | 22496.779 | 444.975 | 444.634 | 544 |
| MapleSTP-mt | 0.000 | 22487.264 | 1654.507 | 447.689 | 395 |
| MapleSTP | 0.000 | 21764.885 | 524.828 | 524.451 | 450 |
| stp-minisat-st | 0.000 | 20582.614 | 634.291 | 633.854 | 1058 |
| ABC_default | 0.000 | 18528.788 | 477.837 | 478.664 | 1354 |
| Q3B | 719.723 | 10397.757 | 4031.130 | 1374.292 | 4430 |
n. Non-competitive.
1. Scores are computed according to Section 7 of the rules.