The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFLIRA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 1683 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | Vampire | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1601 | 196956.463 | 196929.576 | 1601 | 54 | 1547 | 82 | 72 | 10 | |
| Z3n | 0 | 1600 | 114014.906 | 114393.634 | 1600 | 54 | 1546 | 83 | 27 | 7 | |
| 2018-Z3n | 0 | 1600 | 151356.061 | 151704.424 | 1600 | 54 | 1546 | 83 | 47 | 2 | |
| CVC4 | 0 | 1560 | 299439.485 | 302020.23 | 1560 | 0 | 1560 | 123 | 121 | 0 | |
| Vampire | 0 | 1560 | 328984.747 | 303980.273 | 1560 | 0 | 1560 | 123 | 123 | 0 | |
| CVC4-SymBreakn | 0 | 1559 | 298994.282 | 303708.214 | 1559 | 0 | 1559 | 124 | 122 | 0 | |
| Alt-Ergo | 0 | 1506 | 439198.367 | 428684.686 | 1506 | 0 | 1506 | 177 | 177 | 0 | |
| veriT | 0 | 1323 | 845872.953 | 845669.876 | 1323 | 0 | 1323 | 360 | 289 | 5 | |
| SMTInterpol | 0 | 157 | 3640288.714 | 3575591.031 | 157 | 0 | 157 | 1526 | 1468 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 60210.642 | 59844.176 | 0 | 0 | 0 | 1683 | 23 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 60314.703 | 57557.642 | 0 | 0 | 0 | 1683 | 22 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 60367.21 | 57226.853 | 0 | 0 | 0 | 1683 | 22 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1601 | 196956.463 | 196929.576 | 1601 | 54 | 1547 | 82 | 72 | 10 | |
| Z3n | 0 | 1600 | 114021.376 | 114392.634 | 1600 | 54 | 1546 | 83 | 27 | 7 | |
| 2018-Z3n | 0 | 1600 | 151370.151 | 151702.804 | 1600 | 54 | 1546 | 83 | 47 | 2 | |
| Vampire | 0 | 1563 | 348500.047 | 301838.783 | 1563 | 0 | 1563 | 120 | 120 | 0 | |
| CVC4 | 0 | 1560 | 301933.225 | 302014.97 | 1560 | 0 | 1560 | 123 | 121 | 0 | |
| CVC4-SymBreakn | 0 | 1559 | 303469.062 | 303702.214 | 1559 | 0 | 1559 | 124 | 122 | 0 | |
| Alt-Ergo | 0 | 1519 | 485607.727 | 412866.757 | 1519 | 0 | 1519 | 164 | 161 | 0 | |
| veriT | 0 | 1323 | 845923.253 | 845658.766 | 1323 | 0 | 1323 | 360 | 289 | 5 | |
| SMTInterpol | 0 | 157 | 3983938.964 | 3464247.127 | 157 | 0 | 157 | 1526 | 1315 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 60367.21 | 57226.853 | 0 | 0 | 0 | 1683 | 22 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 60314.703 | 57557.642 | 0 | 0 | 0 | 1683 | 22 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 62605.111 | 59843.716 | 0 | 0 | 0 | 1683 | 23 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 54 | 2508.853 | 2460.406 | 54 | 54 | 0 | 1629 | 72 | 10 |
| 2018-Z3n | 0 | 54 | 2461.578 | 2461.583 | 54 | 54 | 0 | 1629 | 47 | 2 |
| Z3n | 0 | 54 | 2463.918 | 2461.834 | 54 | 54 | 0 | 1629 | 27 | 7 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 185.004 | 121.574 | 0 | 0 | 0 | 1683 | 23 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 210.37 | 128.334 | 0 | 0 | 0 | 1683 | 22 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 207.372 | 138.587 | 0 | 0 | 0 | 1683 | 22 | 0 |
| CVC4 | 0 | 0 | 128411.319 | 128401.482 | 0 | 0 | 0 | 1683 | 121 | 0 |
| CVC4-SymBreakn | 0 | 0 | 128449.249 | 128450.649 | 0 | 0 | 0 | 1683 | 122 | 0 |
| veriT | 0 | 0 | 129751.662 | 129751.659 | 0 | 0 | 0 | 1683 | 289 | 5 |
| Alt-Ergo | 0 | 0 | 144930.81 | 130434.44 | 0 | 0 | 0 | 1683 | 161 | 0 |
| Vampire | 0 | 0 | 139200.09 | 131993.91 | 0 | 0 | 0 | 1683 | 120 | 0 |
| SMTInterpol | 0 | 0 | 132000.0 | 132000.0 | 0 | 0 | 0 | 1683 | 1315 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1563 | 53299.957 | 13844.873 | 1563 | 0 | 1563 | 120 | 120 | 0 |
| CVC4 | 0 | 1560 | 17521.906 | 17613.488 | 1560 | 0 | 1560 | 123 | 121 | 0 |
| CVC4-SymBreakn | 0 | 1559 | 19019.813 | 19251.565 | 1559 | 0 | 1559 | 124 | 122 | 0 |
| Par4 | 0 | 1547 | 38447.61 | 38469.17 | 1547 | 0 | 1547 | 136 | 72 | 10 |
| Z3n | 0 | 1546 | 36477.373 | 36477.597 | 1546 | 0 | 1546 | 137 | 27 | 7 |
| 2018-Z3n | 0 | 1546 | 38119.459 | 38122.276 | 1546 | 0 | 1546 | 137 | 47 | 2 |
| Alt-Ergo | 0 | 1519 | 184676.917 | 126432.317 | 1519 | 0 | 1519 | 164 | 161 | 0 |
| veriT | 0 | 1323 | 561386.111 | 561120.787 | 1323 | 0 | 1323 | 360 | 289 | 5 |
| SMTInterpol | 0 | 157 | 3696542.644 | 3177978.561 | 157 | 0 | 157 | 1526 | 1315 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 59925.825 | 56954.069 | 0 | 0 | 0 | 1683 | 22 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 59882.92 | 57265.647 | 0 | 0 | 0 | 1683 | 22 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 62190.996 | 59569.552 | 0 | 0 | 0 | 1683 | 23 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1601 | 2124.463 | 2097.576 | 1601 | 54 | 1547 | 82 | 72 | 10 | |
| Z3n | 0 | 1600 | 1909.93 | 1907.319 | 1600 | 54 | 1546 | 83 | 65 | 7 | |
| 2018-Z3n | 0 | 1600 | 2175.508 | 2175.609 | 1600 | 54 | 1546 | 83 | 81 | 2 | |
| Vampire | 0 | 1516 | 9638.991 | 5659.215 | 1516 | 0 | 1516 | 167 | 167 | 0 | |
| CVC4-SymBreakn | 0 | 1490 | 4782.005 | 4781.607 | 1490 | 0 | 1490 | 193 | 193 | 0 | |
| CVC4 | 0 | 1489 | 4790.392 | 4788.378 | 1489 | 0 | 1489 | 194 | 194 | 0 | |
| Alt-Ergo | 0 | 1483 | 5536.658 | 5058.654 | 1483 | 0 | 1483 | 200 | 200 | 0 | |
| veriT | 0 | 1301 | 13585.596 | 13548.749 | 1301 | 0 | 1301 | 382 | 377 | 5 | |
| SMTInterpol | 0 | 138 | 37575.401 | 37406.221 | 138 | 0 | 138 | 1545 | 1545 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 6498.559 | 4318.984 | 0 | 0 | 0 | 1683 | 27 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 6329.926 | 4536.488 | 0 | 0 | 0 | 1683 | 28 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 6464.746 | 4648.706 | 0 | 0 | 0 | 1683 | 27 | 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.