The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDTLIA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 278 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | — | cvc5 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 193 | 58307.482 | 60034.719 | 193 | 0 | 193 | 85 | 85 | 0 |
| 2022-cvc5n | 0 | 191 | 56609.119 | 58260.68 | 191 | 0 | 191 | 87 | 87 | 0 |
| Vampire | 0 | 129 | 4012.197 | 1023.308 | 129 | 0 | 129 | 149 | 149 | 0 |
| iProver Fixedn | 0 | 25 | 3970.815 | 1024.509 | 25 | 0 | 25 | 253 | 253 | 0 |
| iProver | 0 | 24 | 3760.276 | 968.882 | 24 | 0 | 24 | 254 | 254 | 0 |
| SMTInterpol | 0 | 20 | 2914.892 | 2531.838 | 20 | 0 | 20 | 258 | 257 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 193 | 58307.482 | 60034.719 | 193 | 0 | 193 | 85 | 85 | 0 |
| 2022-cvc5n | 0 | 191 | 56609.119 | 58260.68 | 191 | 0 | 191 | 87 | 87 | 0 |
| Vampire | 0 | 131 | 13314.717 | 3366.128 | 131 | 0 | 131 | 147 | 147 | 0 |
| iProver | 0 | 27 | 12482.236 | 3176.295 | 27 | 0 | 27 | 251 | 251 | 0 |
| iProver Fixedn | 0 | 26 | 6723.415 | 1722.536 | 26 | 0 | 26 | 252 | 252 | 0 |
| SMTInterpol | 0 | 20 | 2914.892 | 2531.838 | 20 | 0 | 20 | 258 | 257 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 278 | 87 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 278 | 147 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 278 | 85 | 0 |
| SMTInterpol | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 278 | 257 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 278 | 251 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 278 | 252 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 193 | 58307.482 | 60034.719 | 193 | 0 | 193 | 9 | 76 | 85 | 0 |
| 2022-cvc5n | 0 | 191 | 56609.119 | 58260.68 | 191 | 0 | 191 | 11 | 76 | 87 | 0 |
| Vampire | 0 | 131 | 13314.717 | 3366.128 | 131 | 0 | 131 | 71 | 76 | 147 | 0 |
| iProver | 0 | 27 | 12482.236 | 3176.295 | 27 | 0 | 27 | 175 | 76 | 251 | 0 |
| iProver Fixedn | 0 | 26 | 6723.415 | 1722.536 | 26 | 0 | 26 | 176 | 76 | 252 | 0 |
| SMTInterpol | 0 | 20 | 2914.892 | 2531.838 | 20 | 0 | 20 | 182 | 76 | 257 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 106 | 892.077 | 235.462 | 106 | 0 | 106 | 172 | 172 | 0 |
| cvc5 | 0 | 25 | 22.915 | 22.911 | 25 | 0 | 25 | 253 | 253 | 0 |
| 2022-cvc5n | 0 | 24 | 41.633 | 41.624 | 24 | 0 | 24 | 254 | 254 | 0 |
| SMTInterpol | 0 | 11 | 49.654 | 21.151 | 11 | 0 | 11 | 267 | 267 | 0 |
| iProver Fixedn | 0 | 11 | 176.088 | 48.761 | 11 | 0 | 11 | 267 | 267 | 0 |
| iProver | 0 | 10 | 143.707 | 40.072 | 10 | 0 | 10 | 268 | 268 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.