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 Fri Oct 30 12:49:29 GMT
Competition benchmarks = 26414
Competition industrial benchmarks = 24914
| Sequential Performance | Sequential Performance (industrial) | Parallel Performance | Parallel Performance (industrial) |
|---|---|---|---|
| Boolector (QF_BV) | Boolector (QF_BV) | Boolector (QF_BV) | Boolector (QF_BV) |
| Solver | Errors | Corrects | CPU |
|---|---|---|---|
| Boolector (QF_BV) | 0 | 26260 | 647474.64 |
| CVC4 | 0 | 26001 | 1256814.65 |
| CVC4 (exp) | 0 | 26138 | 939541.88 |
| SMT-RAT | 14 | 16329 | 25022167.18 |
| STP-CMSat4 | 0 | 26124 | 979823.26 |
| STP-CMSat4 (mt-v15) | 14 | 17486 | 70768.54 |
| STP-CMSat4 (v15) | 16 | 26181 | 756053.05 |
| STP-MiniSAT (v15) | 16 | 25587 | 2265496.19 |
| Yices | 0 | 25647 | 2106185.67 |
| MathSatn | 0 | 25895 | 1658560.27 |
| z3n | 0 | 26108 | 1052484.34 |
| Solver | Errors | Corrects | CPU |
|---|---|---|---|
| Boolector (QF_BV) | 0 | 24814 | 419203.51 |
| CVC4 | 0 | 24656 | 809494.82 |
| CVC4 (exp) | 0 | 24739 | 608467.12 |
| SMT-RAT | 14 | 15236 | 23763359.61 |
| STP-CMSat4 | 0 | 24757 | 526073.10 |
| STP-CMSat4 (mt-v15) | 14 | 17427 | 69848.51 |
| STP-CMSat4 (v15) | 16 | 24749 | 497265.71 |
| STP-MiniSAT (v15) | 16 | 24679 | 664494.19 |
| Yices | 0 | 24752 | 535652.74 |
| MathSatn | 0 | 24715 | 650255.89 |
| z3n | 0 | 24769 | 494140.09 |
| Solver | Errors | Corrects | CPU | WALL |
|---|---|---|---|---|
| Boolector (QF_BV) | 0 | 26260 | 647616.94 | 647460.84 |
| CVC4 | 0 | 26083 | 2137611.28 | 1066917.19 |
| CVC4 (exp) | 0 | 26191 | 1479676.87 | 739505.94 |
| SMT-RAT | 14 | 16329 | 25030959.40 | 25021698.23 |
| STP-CMSat4 | 0 | 26124 | 980070.44 | 979739.65 |
| STP-CMSat4 (mt-v15) | 14 | 17486 | 70789.71 | 70751.13 |
| STP-CMSat4 (v15) | 16 | 26181 | 756229.98 | 755904.76 |
| STP-MiniSAT (v15) | 16 | 25587 | 2266235.03 | 2265411.50 |
| Yices | 0 | 25647 | 2106884.50 | 2106222.00 |
| MathSatn | 0 | 25895 | 1658981.54 | 1658449.30 |
| z3n | 0 | 26108 | 1052766.15 | 1052371.69 |
| Solver | Errors | Corrects | CPU | WALL |
|---|---|---|---|---|
| Boolector (QF_BV) | 0 | 24814 | 419295.26 | 419223.17 |
| CVC4 | 0 | 24706 | 1370087.84 | 684664.47 |
| CVC4 (exp) | 0 | 24766 | 949093.38 | 475152.10 |
| SMT-RAT | 14 | 15236 | 23771835.06 | 23762966.85 |
| STP-CMSat4 | 0 | 24757 | 526200.78 | 526054.16 |
| STP-CMSat4 (mt-v15) | 14 | 17427 | 69869.68 | 69829.17 |
| STP-CMSat4 (v15) | 16 | 24749 | 497383.76 | 497219.91 |
| STP-MiniSAT (v15) | 16 | 24679 | 664679.87 | 664482.02 |
| Yices | 0 | 24752 | 535796.91 | 535723.71 |
| MathSatn | 0 | 24715 | 650407.29 | 650222.61 |
| z3n | 0 | 24769 | 494270.76 | 494088.81 |
| Solver | Not Solved | Remaining |
|---|---|---|
| Boolector (QF_BV) | 154 | 0 |
| CVC4 | 331 | 0 |
| CVC4 (exp) | 223 | 0 |
| SMT-RAT | 10071 | 0 |
| STP-CMSat4 | 290 | 0 |
| STP-CMSat4 (mt-v15) | 8914 | 0 |
| STP-CMSat4 (v15) | 217 | 0 |
| STP-MiniSAT (v15) | 811 | 0 |
| Yices | 767 | 0 |
| MathSatn | 519 | 0 |
| z3n | 306 | 0 |
n. Non-competitive.