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 2020-07-04 11:46:58 +0000
Benchmarks: 1346 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1280 | 79349.713 | 79314.478 | 1280 | 41 | 1239 | 66 | 64 | 2 | |
| CVC4 | 0 | 1246 | 121889.106 | 122603.6 | 1246 | 0 | 1246 | 100 | 99 | 0 | |
| z3n | 0 | 1238 | 94608.574 | 94628.128 | 1238 | 0 | 1238 | 108 | 70 | 0 | |
| Vampire | 0 | 1225 | 149640.278 | 146519.88 | 1225 | 0 | 1225 | 121 | 121 | 0 | |
| Alt-Ergo | 0 | 1206 | 155046.141 | 148710.889 | 1206 | 0 | 1206 | 140 | 120 | 2 | |
| veriT | 0 | 1073 | 327539.443 | 327585.059 | 1073 | 0 | 1073 | 273 | 272 | 0 | |
| veriT+viten | 0 | 1071 | 330065.753 | 330085.935 | 1071 | 0 | 1071 | 275 | 202 | 73 | |
| SMTInterpol-fixedn | 0 | 995 | 423622.196 | 421760.142 | 995 | 0 | 995 | 351 | 348 | 0 | |
| SMTInterpol | 0 | 995 | 423936.011 | 421945.718 | 995 | 0 | 995 | 351 | 348 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 44721.524 | 40887.366 | 0 | 0 | 0 | 1346 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1280 | 79349.713 | 79314.478 | 1280 | 41 | 1239 | 66 | 64 | 2 | |
| Vampire | 0 | 1248 | 166260.748 | 129581.665 | 1248 | 0 | 1248 | 98 | 98 | 0 | |
| CVC4 | 0 | 1246 | 122588.736 | 122599.67 | 1246 | 0 | 1246 | 100 | 99 | 0 | |
| z3n | 0 | 1238 | 94623.044 | 94625.568 | 1238 | 0 | 1238 | 108 | 70 | 0 | |
| Alt-Ergo | 0 | 1217 | 173319.081 | 142481.244 | 1217 | 0 | 1217 | 129 | 109 | 2 | |
| veriT | 0 | 1073 | 327574.453 | 327575.269 | 1073 | 0 | 1073 | 273 | 272 | 0 | |
| veriT+viten | 0 | 1071 | 330078.823 | 330079.485 | 1071 | 0 | 1071 | 275 | 202 | 73 | |
| SMTInterpol | 0 | 995 | 442284.741 | 416608.205 | 995 | 0 | 995 | 351 | 333 | 0 | |
| SMTInterpol-fixedn | 0 | 995 | 433182.626 | 417552.381 | 995 | 0 | 995 | 351 | 338 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 44721.524 | 40887.366 | 0 | 0 | 0 | 1346 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 41 | 1311.384 | 1260.123 | 41 | 41 | 0 | 1305 | 64 | 2 |
| UltimateEliminator+MathSAT | 0 | 0 | 167.487 | 107.533 | 0 | 0 | 0 | 1346 | 30 | 0 |
| z3n | 0 | 0 | 43408.828 | 43408.839 | 0 | 0 | 0 | 1346 | 70 | 0 |
| SMTInterpol-fixedn | 0 | 0 | 48995.933 | 48360.516 | 0 | 0 | 0 | 1346 | 338 | 0 |
| Alt-Ergo | 0 | 0 | 49200.4 | 49200.13 | 0 | 0 | 0 | 1346 | 109 | 2 |
| SMTInterpol | 0 | 0 | 49225.143 | 49212.794 | 0 | 0 | 0 | 1346 | 333 | 0 |
| CVC4 | 0 | 0 | 49474.22 | 49474.347 | 0 | 0 | 0 | 1346 | 99 | 0 |
| veriT | 0 | 0 | 49876.34 | 49876.487 | 0 | 0 | 0 | 1346 | 272 | 0 |
| veriT+viten | 0 | 0 | 50400.0 | 50400.0 | 0 | 0 | 0 | 1346 | 202 | 73 |
| Vampire | 0 | 0 | 50400.0 | 50400.0 | 0 | 0 | 0 | 1346 | 98 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1248 | 48660.408 | 15585.495 | 1248 | 0 | 1248 | 98 | 98 | 0 |
| CVC4 | 0 | 1246 | 9514.516 | 9525.323 | 1246 | 0 | 1246 | 100 | 99 | 0 |
| 2019-Par4n | 0 | 1239 | 14438.329 | 14454.354 | 1239 | 0 | 1239 | 107 | 64 | 2 |
| z3n | 0 | 1238 | 14826.481 | 14826.661 | 1238 | 0 | 1238 | 108 | 70 | 0 |
| Alt-Ergo | 0 | 1217 | 75901.492 | 48868.345 | 1217 | 0 | 1217 | 129 | 109 | 2 |
| veriT | 0 | 1073 | 214098.113 | 214098.782 | 1073 | 0 | 1073 | 273 | 272 | 0 |
| veriT+viten | 0 | 1071 | 216078.823 | 216079.485 | 1071 | 0 | 1071 | 275 | 202 | 73 |
| SMTInterpol | 0 | 995 | 329039.148 | 304392.215 | 995 | 0 | 995 | 351 | 333 | 0 |
| SMTInterpol-fixedn | 0 | 995 | 319951.773 | 306130.978 | 995 | 0 | 995 | 351 | 338 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 44367.757 | 40652.648 | 0 | 0 | 0 | 1346 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1280 | 1733.713 | 1698.478 | 1280 | 41 | 1239 | 66 | 64 | 2 | |
| z3n | 0 | 1238 | 2383.554 | 2383.694 | 1238 | 0 | 1238 | 108 | 94 | 0 | |
| Vampire | 0 | 1214 | 4347.846 | 3590.148 | 1214 | 0 | 1214 | 132 | 132 | 0 | |
| CVC4 | 0 | 1198 | 3663.935 | 3663.643 | 1198 | 0 | 1198 | 148 | 148 | 0 | |
| Alt-Ergo | 0 | 1189 | 4230.507 | 3638.529 | 1189 | 0 | 1189 | 157 | 138 | 2 | |
| veriT+viten | 0 | 1071 | 6678.823 | 6679.485 | 1071 | 0 | 1071 | 275 | 202 | 73 | |
| veriT | 0 | 1070 | 6690.062 | 6690.721 | 1070 | 0 | 1070 | 276 | 276 | 0 | |
| SMTInterpol-fixedn | 0 | 987 | 9417.32 | 9072.215 | 987 | 0 | 987 | 359 | 358 | 0 | |
| SMTInterpol | 0 | 987 | 9422.607 | 9072.718 | 987 | 0 | 987 | 359 | 358 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 5775.429 | 4218.25 | 0 | 0 | 0 | 1346 | 43 | 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.