The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the ALIA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:04 +0000
Benchmarks: 19 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| SMTInterpol | SMTInterpol | SMTInterpol | cvc5 | SMTInterpol |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 19 | 0.935 | 0.938 | 19 | 1 | 18 | 0 | 0 | 0 |
| 2018-Z3n | 0 | 19 | 1.209 | 1.211 | 19 | 1 | 18 | 0 | 0 | 0 |
| 2020-z3n | 0 | 19 | 1.295 | 1.301 | 19 | 1 | 18 | 0 | 0 | 0 |
| SMTInterpol | 0 | 19 | 150.027 | 59.611 | 19 | 1 | 18 | 0 | 0 | 0 |
| cvc5 | 0 | 18 | 4.241 | 4.235 | 18 | 0 | 18 | 1 | 0 | 0 |
| cvc5 - fixedn | 0 | 18 | 4.307 | 4.297 | 18 | 0 | 18 | 1 | 0 | 0 |
| 2020-CVC4n | 0 | 18 | 5.052 | 5.044 | 18 | 0 | 18 | 1 | 0 | 0 |
| 2020-Vampiren | 0 | 15 | 7546.982 | 5627.297 | 15 | 0 | 15 | 4 | 4 | 0 |
| Vampire - fixedn | 0 | 14 | 7545.226 | 6532.63 | 14 | 0 | 14 | 5 | 5 | 0 |
| Vampire | 0 | 14 | 7707.829 | 6551.647 | 14 | 0 | 14 | 5 | 5 | 0 |
| veriT | 0 | 4 | 17997.719 | 18000.782 | 4 | 0 | 4 | 15 | 15 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 174.068 | 169.979 | 1 | 1 | 0 | 18 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 19 | 0.935 | 0.938 | 19 | 1 | 18 | 0 | 0 | 0 |
| 2018-Z3n | 0 | 19 | 1.209 | 1.211 | 19 | 1 | 18 | 0 | 0 | 0 |
| 2020-z3n | 0 | 19 | 1.295 | 1.301 | 19 | 1 | 18 | 0 | 0 | 0 |
| SMTInterpol | 0 | 19 | 150.027 | 59.611 | 19 | 1 | 18 | 0 | 0 | 0 |
| cvc5 | 0 | 18 | 4.241 | 4.235 | 18 | 0 | 18 | 1 | 0 | 0 |
| cvc5 - fixedn | 0 | 18 | 4.307 | 4.297 | 18 | 0 | 18 | 1 | 0 | 0 |
| 2020-CVC4n | 0 | 18 | 5.052 | 5.044 | 18 | 0 | 18 | 1 | 0 | 0 |
| 2020-Vampiren | 0 | 16 | 8364.822 | 4957.952 | 16 | 0 | 16 | 3 | 3 | 0 |
| Vampire - fixedn | 0 | 15 | 8183.656 | 5823.425 | 15 | 0 | 15 | 4 | 4 | 0 |
| Vampire | 0 | 15 | 8705.239 | 5927.226 | 15 | 0 | 15 | 4 | 4 | 0 |
| veriT | 0 | 4 | 18000.059 | 18000.142 | 4 | 0 | 4 | 15 | 15 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 174.068 | 169.979 | 1 | 1 | 0 | 18 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1 | 0.037 | 0.037 | 1 | 1 | 0 | 0 | 18 | 0 | 0 |
| 2020-z3n | 0 | 1 | 0.052 | 0.052 | 1 | 1 | 0 | 0 | 18 | 0 | 0 |
| 2018-Z3n | 0 | 1 | 0.055 | 0.056 | 1 | 1 | 0 | 0 | 18 | 0 | 0 |
| SMTInterpol | 0 | 1 | 0.68 | 0.759 | 1 | 1 | 0 | 0 | 18 | 0 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 5.108 | 2.942 | 1 | 1 | 0 | 0 | 18 | 0 | 0 |
| cvc5 - fixedn | 0 | 0 | 0.294 | 0.29 | 0 | 0 | 0 | 1 | 18 | 0 | 0 |
| cvc5 | 0 | 0 | 0.289 | 0.292 | 0 | 0 | 0 | 1 | 18 | 0 | 0 |
| 2020-CVC4n | 0 | 0 | 0.304 | 0.301 | 0 | 0 | 0 | 1 | 18 | 0 | 0 |
| 2020-Vampiren | 0 | 0 | 1200.0 | 1200.0 | 0 | 0 | 0 | 1 | 18 | 3 | 0 |
| Vampire | 0 | 0 | 1200.0 | 1200.0 | 0 | 0 | 0 | 1 | 18 | 4 | 0 |
| veriT | 0 | 0 | 1200.0 | 1200.0 | 0 | 0 | 0 | 1 | 18 | 15 | 0 |
| Vampire - fixedn | 0 | 0 | 1200.0 | 1200.0 | 0 | 0 | 0 | 1 | 18 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 18 | 0.898 | 0.9 | 18 | 0 | 18 | 0 | 1 | 0 | 0 |
| 2018-Z3n | 0 | 18 | 1.153 | 1.156 | 18 | 0 | 18 | 0 | 1 | 0 | 0 |
| 2020-z3n | 0 | 18 | 1.243 | 1.249 | 18 | 0 | 18 | 0 | 1 | 0 | 0 |
| cvc5 | 0 | 18 | 3.951 | 3.943 | 18 | 0 | 18 | 0 | 1 | 0 | 0 |
| cvc5 - fixedn | 0 | 18 | 4.013 | 4.006 | 18 | 0 | 18 | 0 | 1 | 0 | 0 |
| 2020-CVC4n | 0 | 18 | 4.748 | 4.743 | 18 | 0 | 18 | 0 | 1 | 0 | 0 |
| SMTInterpol | 0 | 18 | 149.347 | 58.852 | 18 | 0 | 18 | 0 | 1 | 0 | 0 |
| 2020-Vampiren | 0 | 16 | 7164.822 | 3757.952 | 16 | 0 | 16 | 2 | 1 | 3 | 0 |
| Vampire - fixedn | 0 | 15 | 6983.656 | 4623.425 | 15 | 0 | 15 | 3 | 1 | 4 | 0 |
| Vampire | 0 | 15 | 7505.239 | 4727.226 | 15 | 0 | 15 | 3 | 1 | 4 | 0 |
| veriT | 0 | 4 | 16800.059 | 16800.142 | 4 | 0 | 4 | 14 | 1 | 15 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 168.961 | 167.037 | 0 | 0 | 0 | 18 | 1 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 19 | 0.935 | 0.938 | 19 | 1 | 18 | 0 | 0 | 0 |
| 2018-Z3n | 0 | 19 | 1.209 | 1.211 | 19 | 1 | 18 | 0 | 0 | 0 |
| 2020-z3n | 0 | 19 | 1.295 | 1.301 | 19 | 1 | 18 | 0 | 0 | 0 |
| SMTInterpol | 0 | 19 | 150.027 | 59.611 | 19 | 1 | 18 | 0 | 0 | 0 |
| cvc5 | 0 | 18 | 4.241 | 4.235 | 18 | 0 | 18 | 1 | 0 | 0 |
| cvc5 - fixedn | 0 | 18 | 4.307 | 4.297 | 18 | 0 | 18 | 1 | 0 | 0 |
| 2020-CVC4n | 0 | 18 | 5.052 | 5.044 | 18 | 0 | 18 | 1 | 0 | 0 |
| 2020-Vampiren | 0 | 9 | 275.632 | 255.599 | 9 | 0 | 9 | 10 | 10 | 0 |
| Vampire | 0 | 8 | 289.462 | 276.732 | 8 | 0 | 8 | 11 | 11 | 0 |
| Vampire - fixedn | 0 | 7 | 301.556 | 294.833 | 7 | 0 | 7 | 12 | 12 | 0 |
| veriT | 0 | 4 | 360.059 | 360.142 | 4 | 0 | 4 | 15 | 15 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 185.878 | 97.985 | 1 | 1 | 0 | 18 | 1 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.