The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the BV division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 823 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 770 | 145888.247 | 132036.228 | 770 | 221 | 549 | 53 | 53 | 0 | |
| Q3B | 0 | 736 | 210609.263 | 203206.795 | 736 | 222 | 514 | 87 | 77 | 5 | |
| 2018-CVC4n | 0 | 722 | 288362.963 | 292450.698 | 722 | 191 | 531 | 101 | 101 | 0 | |
| CVC4 | 0 | 722 | 329819.695 | 335480.056 | 722 | 189 | 533 | 101 | 101 | 0 | |
| Poolector | 0 | 702 | 315355.176 | 296839.783 | 702 | 219 | 483 | 121 | 121 | 0 | |
| Boolector | 0 | 691 | 338246.91 | 328328.358 | 691 | 210 | 481 | 132 | 132 | 0 | |
| Z3n | 0 | 688 | 331791.805 | 331816.012 | 688 | 198 | 490 | 135 | 134 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 274 | 364065.202 | 362363.856 | 274 | 9 | 265 | 549 | 138 | 10 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 777 | 162126.297 | 123607.51 | 777 | 226 | 551 | 46 | 46 | 0 | |
| Q3B | 0 | 741 | 218253.473 | 198536.805 | 741 | 225 | 516 | 82 | 72 | 5 | |
| 2018-CVC4n | 0 | 722 | 291188.913 | 292445.478 | 722 | 191 | 531 | 101 | 101 | 0 | |
| CVC4 | 0 | 722 | 333430.045 | 335475.076 | 722 | 189 | 533 | 101 | 101 | 0 | |
| Poolector | 0 | 711 | 343502.886 | 287805.665 | 711 | 223 | 488 | 112 | 112 | 0 | |
| Boolector | 0 | 698 | 344389.78 | 323873.368 | 698 | 214 | 484 | 125 | 125 | 0 | |
| Z3n | 0 | 688 | 331830.275 | 331810.002 | 688 | 198 | 490 | 135 | 134 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 274 | 392041.302 | 361021.506 | 274 | 9 | 265 | 549 | 132 | 10 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 226 | 62329.284 | 37328.871 | 226 | 226 | 0 | 597 | 46 | 0 |
| Q3B | 0 | 225 | 44707.621 | 34362.751 | 225 | 225 | 0 | 598 | 72 | 5 |
| Poolector | 0 | 223 | 71316.055 | 44962.488 | 223 | 223 | 0 | 600 | 112 | 0 |
| Boolector | 0 | 214 | 74742.673 | 66401.951 | 214 | 214 | 0 | 609 | 125 | 0 |
| Z3n | 0 | 198 | 96217.297 | 96217.604 | 198 | 198 | 0 | 625 | 134 | 0 |
| 2018-CVC4n | 0 | 191 | 154577.722 | 155633.699 | 191 | 191 | 0 | 632 | 101 | 0 |
| CVC4 | 0 | 189 | 201052.813 | 202877.363 | 189 | 189 | 0 | 634 | 101 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 9 | 234551.169 | 213346.58 | 9 | 9 | 0 | 814 | 132 | 10 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 551 | 42197.013 | 28678.639 | 551 | 0 | 551 | 272 | 46 | 0 |
| CVC4 | 0 | 533 | 74777.232 | 74997.713 | 533 | 0 | 533 | 290 | 101 | 0 |
| 2018-CVC4n | 0 | 531 | 79011.19 | 79211.779 | 531 | 0 | 531 | 292 | 101 | 0 |
| Q3B | 0 | 516 | 115945.853 | 106574.054 | 516 | 0 | 516 | 307 | 72 | 5 |
| Z3n | 0 | 490 | 178012.978 | 177992.398 | 490 | 0 | 490 | 333 | 134 | 0 |
| Poolector | 0 | 488 | 214586.831 | 185243.177 | 488 | 0 | 488 | 335 | 112 | 0 |
| Boolector | 0 | 484 | 212047.107 | 199871.417 | 484 | 0 | 484 | 339 | 125 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 265 | 112383.498 | 106851.539 | 265 | 0 | 265 | 558 | 132 | 10 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 742 | 3643.647 | 2428.24 | 742 | 208 | 534 | 81 | 81 | 0 | |
| Q3B | 0 | 713 | 4031.069 | 3121.869 | 713 | 205 | 508 | 110 | 100 | 5 | |
| Poolector | 0 | 664 | 6433.646 | 4600.048 | 664 | 208 | 456 | 159 | 159 | 0 | |
| Z3n | 0 | 655 | 4475.36 | 4453.575 | 655 | 192 | 463 | 168 | 168 | 0 | |
| Boolector | 0 | 643 | 5108.267 | 4771.941 | 643 | 196 | 447 | 180 | 180 | 0 | |
| CVC4 | 0 | 626 | 5357.724 | 5355.033 | 626 | 108 | 518 | 197 | 197 | 0 | |
| 2018-CVC4n | 0 | 607 | 6058.305 | 6056.133 | 607 | 97 | 510 | 216 | 216 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 272 | 6301.473 | 5504.543 | 272 | 8 | 264 | 551 | 150 | 10 |
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.