The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFLIRA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:05 +0000
Benchmarks: 1683 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | Vampire | — | Vampire | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1608 | 90164.945 | 90135.396 | 1608 | 53 | 1555 | 75 | 74 | 1 |
| 2020-CVC4n | 0 | 1562 | 148513.397 | 149466.452 | 1562 | 0 | 1562 | 121 | 120 | 0 |
| cvc5 - fixedn | 0 | 1555 | 80808.839 | 159244.378 | 1555 | 0 | 1555 | 128 | 126 | 0 |
| z3n | 0 | 1554 | 110384.959 | 110499.17 | 1554 | 0 | 1554 | 129 | 74 | 0 |
| 2020-z3n | 0 | 1554 | 112292.198 | 112314.077 | 1554 | 0 | 1554 | 129 | 81 | 0 |
| cvc5 | 0 | 1553 | 75746.161 | 161455.373 | 1553 | 0 | 1553 | 130 | 128 | 0 |
| Vampire | 0 | 1533 | 184721.149 | 181732.207 | 1533 | 0 | 1533 | 150 | 150 | 0 |
| Vampire - fixedn | 0 | 1514 | 183423.582 | 179351.782 | 1514 | 0 | 1514 | 169 | 148 | 0 |
| 2020-Vampiren | 0 | 1510 | 183402.066 | 179368.739 | 1510 | 0 | 1510 | 173 | 148 | 0 |
| veriT | 0 | 1335 | 416474.05 | 416511.216 | 1335 | 0 | 1335 | 348 | 274 | 73 |
| SMTInterpol | 0 | 1244 | 533778.971 | 532928.15 | 1244 | 0 | 1244 | 439 | 439 | 0 |
| UltimateEliminator+MathSAT | 0 | 12 | 11125.04 | 7715.458 | 12 | 0 | 12 | 1671 | 0 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1608 | 90164.945 | 90135.396 | 1608 | 53 | 1555 | 75 | 74 | 1 |
| 2020-CVC4n | 0 | 1562 | 149417.237 | 149460.382 | 1562 | 0 | 1562 | 121 | 120 | 0 |
| cvc5 - fixedn | 0 | 1555 | 159144.564 | 159237.778 | 1555 | 0 | 1555 | 128 | 126 | 0 |
| Vampire | 0 | 1555 | 210663.939 | 168565.556 | 1555 | 0 | 1555 | 128 | 128 | 0 |
| z3n | 0 | 1554 | 110462.959 | 110495.9 | 1554 | 0 | 1554 | 129 | 74 | 0 |
| 2020-z3n | 0 | 1554 | 112307.408 | 112310.507 | 1554 | 0 | 1554 | 129 | 81 | 0 |
| cvc5 | 0 | 1553 | 161372.051 | 161449.143 | 1553 | 0 | 1553 | 130 | 128 | 0 |
| Vampire - fixedn | 0 | 1542 | 215644.902 | 162798.213 | 1542 | 0 | 1542 | 141 | 120 | 0 |
| 2020-Vampiren | 0 | 1538 | 209414.926 | 160372.923 | 1538 | 0 | 1538 | 145 | 120 | 0 |
| veriT | 0 | 1335 | 416499.58 | 416500.636 | 1335 | 0 | 1335 | 348 | 274 | 73 |
| SMTInterpol | 0 | 1244 | 539217.691 | 530571.359 | 1244 | 0 | 1244 | 439 | 434 | 0 |
| UltimateEliminator+MathSAT | 0 | 12 | 11125.04 | 7715.458 | 12 | 0 | 12 | 1671 | 0 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 53 | 1313.427 | 1262.452 | 53 | 53 | 0 | 1 | 1629 | 74 | 1 |
| UltimateEliminator+MathSAT | 0 | 0 | 288.151 | 181.405 | 0 | 0 | 0 | 54 | 1629 | 0 | 2 |
| 2020-z3n | 0 | 0 | 55259.758 | 55259.925 | 0 | 0 | 0 | 54 | 1629 | 81 | 0 |
| z3n | 0 | 0 | 60040.961 | 60040.974 | 0 | 0 | 0 | 54 | 1629 | 74 | 0 |
| veriT | 0 | 0 | 63616.32 | 63616.319 | 0 | 0 | 0 | 54 | 1629 | 274 | 73 |
| 2020-CVC4n | 0 | 0 | 63763.475 | 63764.346 | 0 | 0 | 0 | 54 | 1629 | 120 | 0 |
| cvc5 - fixedn | 0 | 0 | 63771.821 | 63774.162 | 0 | 0 | 0 | 54 | 1629 | 126 | 0 |
| cvc5 | 0 | 0 | 63773.96 | 63776.311 | 0 | 0 | 0 | 54 | 1629 | 128 | 0 |
| 2020-Vampiren | 0 | 0 | 64800.0 | 64800.0 | 0 | 0 | 0 | 54 | 1629 | 120 | 0 |
| SMTInterpol | 0 | 0 | 64800.0 | 64800.0 | 0 | 0 | 0 | 54 | 1629 | 434 | 0 |
| Vampire | 0 | 0 | 64800.0 | 64800.0 | 0 | 0 | 0 | 54 | 1629 | 128 | 0 |
| Vampire - fixedn | 0 | 0 | 64800.0 | 64800.0 | 0 | 0 | 0 | 54 | 1629 | 120 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 1562 | 11253.762 | 11296.036 | 1562 | 0 | 1562 | 5 | 116 | 120 | 0 |
| 2019-Par4n | 0 | 1555 | 14451.518 | 14472.944 | 1555 | 0 | 1555 | 12 | 116 | 74 | 1 |
| cvc5 - fixedn | 0 | 1555 | 20972.743 | 21063.616 | 1555 | 0 | 1555 | 12 | 116 | 126 | 0 |
| Vampire | 0 | 1555 | 71463.939 | 29365.556 | 1555 | 0 | 1555 | 12 | 116 | 128 | 0 |
| z3n | 0 | 1554 | 11886.064 | 11886.94 | 1554 | 0 | 1554 | 13 | 116 | 74 | 0 |
| 2020-z3n | 0 | 1554 | 15435.997 | 15437.244 | 1554 | 0 | 1554 | 13 | 116 | 81 | 0 |
| cvc5 | 0 | 1553 | 23198.091 | 23272.832 | 1553 | 0 | 1553 | 14 | 116 | 128 | 0 |
| Vampire - fixedn | 0 | 1542 | 76444.902 | 23598.213 | 1542 | 0 | 1542 | 25 | 116 | 120 | 0 |
| 2020-Vampiren | 0 | 1538 | 70214.926 | 21172.923 | 1538 | 0 | 1538 | 29 | 116 | 120 | 0 |
| veriT | 0 | 1335 | 278483.26 | 278484.317 | 1335 | 0 | 1335 | 232 | 116 | 274 | 73 |
| SMTInterpol | 0 | 1244 | 395619.351 | 392493.691 | 1244 | 0 | 1244 | 323 | 116 | 434 | 0 |
| UltimateEliminator+MathSAT | 0 | 12 | 10525.613 | 7345.532 | 12 | 0 | 12 | 1555 | 116 | 0 | 2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1608 | 1964.945 | 1935.396 | 1608 | 53 | 1555 | 75 | 74 | 1 |
| 2020-z3n | 0 | 1554 | 2918.589 | 2919.571 | 1554 | 0 | 1554 | 129 | 116 | 0 |
| z3n | 0 | 1551 | 3091.359 | 3091.555 | 1551 | 0 | 1551 | 132 | 116 | 0 |
| Vampire | 0 | 1517 | 5733.839 | 4582.249 | 1517 | 0 | 1517 | 166 | 166 | 0 |
| cvc5 - fixedn | 0 | 1498 | 4556.259 | 4555.536 | 1498 | 0 | 1498 | 185 | 185 | 0 |
| cvc5 | 0 | 1498 | 4556.595 | 4556.113 | 1498 | 0 | 1498 | 185 | 185 | 0 |
| 2020-CVC4n | 0 | 1498 | 4575.448 | 4575.1 | 1498 | 0 | 1498 | 185 | 185 | 0 |
| Vampire - fixedn | 0 | 1496 | 5764.682 | 4584.774 | 1496 | 0 | 1496 | 187 | 166 | 0 |
| 2020-Vampiren | 0 | 1490 | 5527.469 | 4569.212 | 1490 | 0 | 1490 | 193 | 168 | 0 |
| veriT | 0 | 1335 | 8427.58 | 8428.636 | 1335 | 0 | 1335 | 348 | 274 | 73 |
| SMTInterpol | 0 | 1221 | 12225.974 | 11732.255 | 1221 | 0 | 1221 | 462 | 462 | 0 |
| UltimateEliminator+MathSAT | 0 | 12 | 8773.04 | 5363.458 | 12 | 0 | 12 | 1671 | 0 | 2 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.