The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFDTNIRA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:44 +0000
Benchmarks: 762 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | — | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 603 | 141883.565 | 141903.765 | 603 | 0 | 603 | 159 | 118 | 0 |
| 2020-CVC4n | 0 | 599 | 46147.833 | 46162.199 | 599 | 0 | 599 | 163 | 38 | 0 |
| z3-4.8.17n | 0 | 599 | 191296.237 | 191613.893 | 599 | 0 | 599 | 163 | 158 | 0 |
| Vampire | 0 | 581 | 329198.948 | 245494.661 | 581 | 0 | 581 | 181 | 181 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 3542.411 | 2091.22 | 0 | 0 | 0 | 762 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 603 | 141900.635 | 141899.425 | 603 | 0 | 603 | 159 | 118 | 0 |
| 2020-CVC4n | 0 | 599 | 46160.273 | 46160.199 | 599 | 0 | 599 | 163 | 38 | 0 |
| z3-4.8.17n | 0 | 599 | 191607.797 | 191607.313 | 599 | 0 | 599 | 163 | 158 | 0 |
| Vampire | 0 | 596 | 372536.448 | 234695.542 | 596 | 0 | 596 | 166 | 166 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 3542.411 | 2091.22 | 0 | 0 | 0 | 762 | 0 | 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 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 38 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 118 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 166 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 0 | 0 |
| z3-4.8.17n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 158 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 603 | 10929.038 | 10928.793 | 603 | 0 | 603 | 11 | 148 | 118 | 0 |
| 2020-CVC4n | 0 | 599 | 10149.101 | 10149.051 | 599 | 0 | 599 | 15 | 148 | 38 | 0 |
| z3-4.8.17n | 0 | 599 | 17577.458 | 17576.73 | 599 | 0 | 599 | 15 | 148 | 158 | 0 |
| Vampire | 0 | 596 | 162534.328 | 57158.662 | 596 | 0 | 596 | 18 | 148 | 166 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 2855.128 | 1684.248 | 0 | 0 | 0 | 614 | 148 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 603 | 3132.635 | 3131.425 | 603 | 0 | 603 | 159 | 118 | 0 |
| 2020-CVC4n | 0 | 598 | 995.369 | 995.187 | 598 | 0 | 598 | 164 | 39 | 0 |
| z3-4.8.17n | 0 | 595 | 4020.049 | 4019.0 | 595 | 0 | 595 | 167 | 165 | 0 |
| Vampire | 0 | 430 | 9965.014 | 8511.957 | 430 | 0 | 430 | 332 | 332 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 3542.411 | 2091.22 | 0 | 0 | 0 | 762 | 0 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.