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 2021-07-18 17:29:06 +0000
Benchmarks: 204 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 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 104 | 177939.953 | 177958.743 | 104 | 44 | 60 | 100 | 100 | 0 |
| 2020-z3n | 0 | 100 | 177872.457 | 177887.465 | 100 | 41 | 59 | 104 | 104 | 0 |
| cvc5 | 0 | 88 | 188382.796 | 188415.309 | 88 | 23 | 65 | 116 | 116 | 0 |
| SMTInterpol | 0 | 20 | 231445.125 | 230637.912 | 20 | 3 | 17 | 184 | 184 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 104 | 177949.943 | 177955.243 | 104 | 44 | 60 | 100 | 100 | 0 |
| 2020-z3n | 0 | 100 | 177881.607 | 177884.035 | 100 | 41 | 59 | 104 | 104 | 0 |
| cvc5 | 0 | 88 | 188403.176 | 188410.469 | 88 | 23 | 65 | 116 | 116 | 0 |
| SMTInterpol | 0 | 22 | 231540.165 | 230489.212 | 22 | 3 | 19 | 182 | 182 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 44 | 94507.612 | 94509.635 | 44 | 44 | 0 | 59 | 101 | 100 | 0 |
| 2020-z3n | 0 | 41 | 95509.815 | 95511.889 | 41 | 41 | 0 | 62 | 101 | 104 | 0 |
| cvc5 | 0 | 23 | 106512.453 | 106514.584 | 23 | 23 | 0 | 80 | 101 | 116 | 0 |
| SMTInterpol | 0 | 3 | 120001.327 | 120000.925 | 3 | 3 | 0 | 100 | 101 | 182 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 65 | 81890.723 | 81895.885 | 65 | 0 | 65 | 36 | 103 | 116 | 0 |
| z3n | 0 | 60 | 83442.331 | 83445.608 | 60 | 0 | 60 | 41 | 103 | 100 | 0 |
| 2020-z3n | 0 | 59 | 82371.793 | 82372.146 | 59 | 0 | 59 | 42 | 103 | 104 | 0 |
| SMTInterpol | 0 | 19 | 111538.838 | 110488.288 | 19 | 0 | 19 | 82 | 103 | 182 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 6 | 4784.69 | 4784.692 | 6 | 4 | 2 | 198 | 198 | 0 |
| 2020-z3n | 0 | 5 | 4789.394 | 4786.613 | 5 | 3 | 2 | 199 | 199 | 0 |
| cvc5 | 0 | 4 | 4817.283 | 4817.288 | 4 | 3 | 1 | 200 | 200 | 0 |
| SMTInterpol | 0 | 4 | 4819.755 | 4818.351 | 4 | 3 | 1 | 200 | 200 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.