The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFNIRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 300 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | Vampire | — | Vampire | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 59 | 284619.164 | 289703.24 | 59 | 0 | 59 | 241 | 237 | 0 | |
| Vampire | 0 | 59 | 292109.1 | 289978.787 | 59 | 0 | 59 | 241 | 241 | 0 | |
| 2019-Par4n | 0 | 59 | 296107.865 | 292682.971 | 59 | 3 | 56 | 241 | 239 | 2 | |
| Alt-Ergo | 0 | 39 | 299182.073 | 297365.758 | 39 | 0 | 39 | 261 | 246 | 1 | |
| z3n | 0 | 38 | 198406.437 | 200470.047 | 38 | 4 | 34 | 262 | 92 | 4 | |
| UltimateEliminator+MathSAT | 0 | 0 | 5842.497 | 6208.753 | 0 | 0 | 0 | 300 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 61 | 301426.23 | 289632.907 | 61 | 0 | 61 | 239 | 239 | 0 | |
| CVC4 | 0 | 59 | 289546.994 | 289689.01 | 59 | 0 | 59 | 241 | 237 | 0 | |
| 2019-Par4n | 0 | 59 | 296107.865 | 292682.971 | 59 | 3 | 56 | 241 | 239 | 2 | |
| Alt-Ergo | 0 | 40 | 310623.263 | 296479.421 | 40 | 0 | 40 | 260 | 245 | 1 | |
| z3n | 0 | 38 | 199078.357 | 200465.837 | 38 | 4 | 34 | 262 | 92 | 4 | |
| UltimateEliminator+MathSAT | 0 | 0 | 5842.497 | 6208.753 | 0 | 0 | 0 | 300 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 4 | 0.166 | 0.167 | 4 | 4 | 0 | 296 | 92 | 4 |
| 2019-Par4n | 0 | 3 | 1200.02 | 1200.052 | 3 | 3 | 0 | 297 | 239 | 2 |
| UltimateEliminator+MathSAT | 0 | 0 | 13.785 | 9.735 | 0 | 0 | 0 | 300 | 4 | 0 |
| CVC4 | 0 | 0 | 2761.162 | 2764.754 | 0 | 0 | 0 | 300 | 237 | 0 |
| Alt-Ergo | 0 | 0 | 3600.14 | 3600.051 | 0 | 0 | 0 | 300 | 245 | 1 |
| Vampire | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 300 | 239 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 61 | 19426.16 | 11239.417 | 61 | 0 | 61 | 239 | 239 | 0 |
| CVC4 | 0 | 59 | 15583.39 | 15721.821 | 59 | 0 | 59 | 241 | 237 | 0 |
| 2019-Par4n | 0 | 56 | 21307.845 | 17882.919 | 56 | 0 | 56 | 244 | 239 | 2 |
| Alt-Ergo | 0 | 40 | 36554.003 | 33506.114 | 40 | 0 | 40 | 260 | 245 | 1 |
| z3n | 0 | 34 | 23231.372 | 23437.286 | 34 | 0 | 34 | 266 | 92 | 4 |
| UltimateEliminator+MathSAT | 0 | 0 | 1434.22 | 1601.675 | 0 | 0 | 0 | 300 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 51 | 6597.193 | 6137.142 | 51 | 0 | 51 | 249 | 249 | 0 | |
| 2019-Par4n | 0 | 42 | 6207.875 | 6203.774 | 42 | 3 | 39 | 258 | 256 | 2 | |
| CVC4 | 0 | 39 | 6252.871 | 6249.502 | 39 | 0 | 39 | 261 | 258 | 0 | |
| z3n | 0 | 38 | 5826.7 | 5826.705 | 38 | 4 | 34 | 262 | 238 | 4 | |
| Alt-Ergo | 0 | 35 | 6370.143 | 6193.589 | 35 | 0 | 35 | 265 | 254 | 1 | |
| UltimateEliminator+MathSAT | 0 | 0 | 1198.772 | 874.34 | 0 | 0 | 0 | 300 | 7 | 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.