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 2021-07-18 17:29:05 +0000
Benchmarks: 300 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | Vampire | — | Vampire | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 205 | 44676.858 | 44686.764 | 205 | 0 | 205 | 95 | 37 | 0 |
| cvc5 - fixedn | 0 | 205 | 44680.152 | 44689.519 | 205 | 0 | 205 | 95 | 37 | 0 |
| 2020-CVC4n | 0 | 201 | 48013.16 | 48030.156 | 201 | 0 | 201 | 99 | 40 | 0 |
| 2020-Vampiren | 0 | 200 | 158158.235 | 117402.798 | 200 | 0 | 200 | 100 | 84 | 0 |
| Vampire - fixedn | 0 | 191 | 190305.972 | 147150.177 | 191 | 0 | 191 | 109 | 108 | 0 |
| Vampire | 0 | 186 | 197380.078 | 153555.335 | 186 | 0 | 186 | 114 | 114 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Vampiren | 0 | 238 | 235896.345 | 68009.865 | 238 | 0 | 238 | 62 | 5 | 0 |
| Vampire | 0 | 207 | 205540.358 | 137253.895 | 207 | 0 | 207 | 93 | 93 | 0 |
| cvc5 | 0 | 205 | 44684.458 | 44684.914 | 205 | 0 | 205 | 95 | 37 | 0 |
| cvc5 - fixedn | 0 | 205 | 44687.842 | 44687.879 | 205 | 0 | 205 | 95 | 37 | 0 |
| Vampire - fixedn | 0 | 205 | 196032.852 | 136492.868 | 205 | 0 | 205 | 95 | 94 | 0 |
| 2020-CVC4n | 0 | 201 | 48028.49 | 48028.456 | 201 | 0 | 201 | 99 | 40 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Vampiren | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 300 | 5 | 0 |
| 2020-CVC4n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 300 | 40 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 300 | 37 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 300 | 93 | 0 |
| Vampire - fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 300 | 94 | 0 |
| cvc5 - fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 300 | 37 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Vampiren | 0 | 238 | 173372.225 | 51299.804 | 238 | 0 | 238 | 29 | 33 | 5 | 0 |
| Vampire | 0 | 207 | 165940.358 | 97653.895 | 207 | 0 | 207 | 60 | 33 | 93 | 0 |
| cvc5 | 0 | 205 | 17071.653 | 17071.648 | 205 | 0 | 205 | 62 | 33 | 37 | 0 |
| cvc5 - fixedn | 0 | 205 | 17075.131 | 17075.156 | 205 | 0 | 205 | 62 | 33 | 37 | 0 |
| Vampire - fixedn | 0 | 205 | 156432.852 | 96892.868 | 205 | 0 | 205 | 62 | 33 | 94 | 0 |
| 2020-CVC4n | 0 | 201 | 19227.486 | 19227.455 | 201 | 0 | 201 | 66 | 33 | 40 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 203 | 1013.057 | 1013.047 | 203 | 0 | 203 | 97 | 39 | 0 |
| cvc5 | 0 | 203 | 1012.75 | 1013.156 | 203 | 0 | 203 | 97 | 39 | 0 |
| 2020-CVC4n | 0 | 201 | 988.49 | 988.456 | 201 | 0 | 201 | 99 | 40 | 0 |
| Vampire - fixedn | 0 | 117 | 5036.262 | 4690.442 | 117 | 0 | 117 | 183 | 183 | 0 |
| Vampire | 0 | 117 | 5150.248 | 4748.873 | 117 | 0 | 117 | 183 | 183 | 0 |
| 2020-Vampiren | 0 | 105 | 5187.974 | 4876.336 | 105 | 0 | 105 | 195 | 192 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.