The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Datatypes division in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 401 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | SMTInterpol |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-z3-4.8.17n | 0 | 201 | 90328.833 | 90338.814 | 201 | 47 | 154 | 200 | 0 | 200 | 0 |
| cvc5 | 0 | 182 | 92586.967 | 92546.261 | 182 | 47 | 135 | 219 | 0 | 219 | 0 |
| SMTInterpol | 0 | 67 | 29112.469 | 23064.221 | 67 | 39 | 28 | 334 | 0 | 334 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-z3-4.8.17n | 0 | 201 | 90328.833 | 90338.814 | 201 | 47 | 154 | 200 | 0 | 200 | 0 |
| cvc5 | 0 | 182 | 92586.967 | 92546.261 | 182 | 47 | 135 | 219 | 0 | 219 | 0 |
| SMTInterpol | 0 | 85 | 57950.269 | 40363.911 | 85 | 40 | 45 | 316 | 0 | 316 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 47 | 23634.985 | 23640.639 | 47 | 47 | 0 | 153 | 201 | 219 | 0 |
| 2022-z3-4.8.17n | 0 | 47 | 26104.24 | 26106.793 | 47 | 47 | 0 | 153 | 201 | 200 | 0 |
| SMTInterpol | 0 | 40 | 14551.335 | 13819.738 | 40 | 40 | 0 | 160 | 201 | 316 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-z3-4.8.17n | 0 | 154 | 64224.592 | 64232.021 | 154 | 0 | 154 | 47 | 200 | 200 | 0 |
| cvc5 | 0 | 135 | 68951.982 | 68905.622 | 135 | 0 | 135 | 66 | 200 | 219 | 0 |
| SMTInterpol | 0 | 45 | 43398.934 | 26544.173 | 45 | 0 | 45 | 156 | 200 | 316 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| SMTInterpol | 0 | 9 | 228.854 | 131.619 | 9 | 8 | 1 | 392 | 0 | 392 | 0 |
| 2022-z3-4.8.17n | 0 | 3 | 45.011 | 45.007 | 3 | 0 | 3 | 398 | 0 | 398 | 0 |
| cvc5 | 0 | 1 | 16.418 | 16.419 | 1 | 0 | 1 | 400 | 0 | 400 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.