The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFNIRA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:44 +0000
Benchmarks: 300 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | Vampire | cvc5 | Vampire | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 56 | 291263.516 | 296483.41 | 56 | 1 | 55 | 244 | 242 | 0 |
| Vampire | 0 | 49 | 308182.198 | 302967.293 | 49 | 0 | 49 | 251 | 250 | 1 |
| cvc5 | 0 | 47 | 300642.777 | 303636.545 | 47 | 1 | 46 | 253 | 251 | 0 |
| z3-4.8.17n | 0 | 32 | 217077.383 | 220583.815 | 32 | 4 | 28 | 268 | 98 | 5 |
| UltimateEliminator+MathSAT | 0 | 0 | 1486.175 | 888.201 | 0 | 0 | 0 | 300 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 56 | 296282.656 | 296472.03 | 56 | 1 | 55 | 244 | 242 | 0 |
| Vampire | 0 | 52 | 328671.178 | 300872.322 | 52 | 0 | 52 | 248 | 247 | 1 |
| cvc5 | 0 | 47 | 303587.777 | 303625.035 | 47 | 1 | 46 | 253 | 251 | 0 |
| z3-4.8.17n | 0 | 32 | 217096.623 | 220579.395 | 32 | 4 | 28 | 268 | 98 | 5 |
| UltimateEliminator+MathSAT | 0 | 0 | 1486.175 | 888.201 | 0 | 0 | 0 | 300 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 4 | 0.085 | 0.078 | 4 | 4 | 0 | 0 | 296 | 98 | 5 |
| cvc5 | 0 | 1 | 1711.778 | 1712.269 | 1 | 1 | 0 | 3 | 296 | 251 | 0 |
| 2020-CVC4n | 0 | 1 | 2047.969 | 2121.676 | 1 | 1 | 0 | 3 | 296 | 242 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 19.11 | 11.978 | 0 | 0 | 0 | 4 | 296 | 0 | 0 |
| Vampire | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 4 | 296 | 247 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 55 | 14634.687 | 14750.354 | 55 | 0 | 55 | 8 | 237 | 242 | 0 |
| Vampire | 0 | 52 | 26270.008 | 16502.192 | 52 | 0 | 52 | 11 | 237 | 247 | 1 |
| cvc5 | 0 | 46 | 22276.0 | 22312.766 | 46 | 0 | 46 | 17 | 237 | 251 | 0 |
| z3-4.8.17n | 0 | 28 | 29333.797 | 29336.906 | 28 | 0 | 28 | 35 | 237 | 98 | 5 |
| UltimateEliminator+MathSAT | 0 | 0 | 322.398 | 193.233 | 0 | 0 | 0 | 63 | 237 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 41 | 6501.208 | 6293.607 | 41 | 0 | 41 | 259 | 258 | 1 |
| z3-4.8.17n | 0 | 29 | 6415.58 | 6415.525 | 29 | 4 | 25 | 271 | 261 | 5 |
| 2020-CVC4n | 0 | 29 | 6523.967 | 6523.965 | 29 | 0 | 29 | 271 | 270 | 0 |
| cvc5 | 0 | 27 | 6560.116 | 6560.151 | 27 | 0 | 27 | 273 | 271 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 1486.175 | 888.201 | 0 | 0 | 0 | 300 | 0 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.