The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFLIRA logic in the Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 9885 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance |
|---|---|
| cvc5-uc | cvc5-uc |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| cvc5-uc | 0 | 179166 | 78715.355 | 78724.709 | 65 | 0 |
| 2020-CVC4-ucn | 0 | 179064 | 77662.755 | 77681.003 | 64 | 0 |
| z3n | 0 | 178856 | 10341.126 | 10352.952 | 4 | 0 |
| 2020-z3n | 0 | 178847 | 14512.733 | 14516.789 | 3 | 5 |
| Vampire | 0 | 167913 | 55696.036 | 50749.273 | 40 | 0 |
| SMTInterpol | 0 | 152680 | 528406.35 | 524725.329 | 427 | 0 |
| SMTInterpol-remus | 0 | 152356 | 1422316.649 | 1287479.062 | 433 | 0 |
| UltimateEliminator+MathSAT | 0 | 10309 | 54856.17 | 33923.317 | 1 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| cvc5-uc | 0 | 179166 | 78723.815 | 78722.419 | 65 | 0 |
| 2020-CVC4-ucn | 0 | 179064 | 77679.645 | 77678.183 | 64 | 0 |
| z3n | 0 | 178856 | 10342.516 | 10352.792 | 4 | 0 |
| 2020-z3n | 0 | 178847 | 14513.823 | 14516.499 | 3 | 5 |
| Vampire | 0 | 167965 | 91455.036 | 33095.304 | 10 | 0 |
| SMTInterpol-remus | 0 | 152918 | 1428797.769 | 1283718.24 | 421 | 0 |
| SMTInterpol | 0 | 152680 | 531038.96 | 521707.622 | 422 | 0 |
| UltimateEliminator+MathSAT | 0 | 10309 | 54856.17 | 33923.317 | 1 | 2 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.