The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_DT logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 201 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 | smtinterpol |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 106 | 173669.417 | 173688.979 | 106 | 41 | 65 | 95 | 95 | 0 |
| 2021-z3n | 0 | 104 | 172881.246 | 172899.608 | 104 | 40 | 64 | 97 | 97 | 0 |
| cvc5 | 0 | 85 | 188505.366 | 188535.286 | 85 | 21 | 64 | 116 | 116 | 0 |
| smtinterpol | 0 | 7 | 235702.976 | 235032.689 | 7 | 0 | 7 | 194 | 194 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 106 | 173680.147 | 173686.119 | 106 | 41 | 65 | 95 | 95 | 0 |
| 2021-z3n | 0 | 104 | 172890.636 | 172895.778 | 104 | 40 | 64 | 97 | 97 | 0 |
| cvc5 | 0 | 85 | 188523.986 | 188530.246 | 85 | 21 | 64 | 116 | 116 | 0 |
| smtinterpol | 0 | 14 | 236800.506 | 233591.8 | 14 | 0 | 14 | 187 | 187 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 41 | 96276.622 | 96278.905 | 41 | 41 | 0 | 59 | 101 | 95 | 0 |
| 2021-z3n | 0 | 40 | 95702.171 | 95703.967 | 40 | 40 | 0 | 60 | 101 | 97 | 0 |
| cvc5 | 0 | 21 | 104497.477 | 104498.978 | 21 | 21 | 0 | 79 | 101 | 116 | 0 |
| smtinterpol | 0 | 0 | 120000.0 | 120000.0 | 0 | 0 | 0 | 100 | 101 | 187 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 65 | 77403.525 | 77407.214 | 65 | 0 | 65 | 36 | 100 | 95 | 0 |
| 2021-z3n | 0 | 64 | 77188.465 | 77191.811 | 64 | 0 | 64 | 37 | 100 | 97 | 0 |
| cvc5 | 0 | 64 | 84026.509 | 84031.268 | 64 | 0 | 64 | 37 | 100 | 116 | 0 |
| smtinterpol | 0 | 14 | 116800.506 | 113591.8 | 14 | 0 | 14 | 87 | 100 | 187 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 4 | 4784.032 | 4784.028 | 4 | 1 | 3 | 197 | 197 | 0 |
| 2021-z3n | 0 | 4 | 4784.171 | 4784.174 | 4 | 1 | 3 | 197 | 197 | 0 |
| smtinterpol | 0 | 1 | 4818.688 | 4817.69 | 1 | 0 | 1 | 200 | 200 | 0 |
| cvc5 | 0 | 0 | 4824.0 | 4824.0 | 0 | 0 | 0 | 201 | 201 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.