The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFDT logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 200 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 | — |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 105 | 165691.769 | 165719.701 | 105 | 30 | 75 | 95 | 95 | 0 |
| z3-4.8.17n | 0 | 101 | 156619.972 | 156635.693 | 101 | 7 | 94 | 99 | 99 | 0 |
| 2021-z3n | 0 | 101 | 158901.46 | 158914.474 | 101 | 7 | 94 | 99 | 99 | 0 |
| smtinterpol | 0 | 10 | 236445.595 | 234216.568 | 10 | 0 | 10 | 190 | 190 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 105 | 165707.829 | 165715.601 | 105 | 30 | 75 | 95 | 95 | 0 |
| z3-4.8.17n | 0 | 101 | 156628.411 | 156632.503 | 101 | 7 | 94 | 99 | 99 | 0 |
| 2021-z3n | 0 | 101 | 158908.46 | 158911.404 | 101 | 7 | 94 | 99 | 99 | 0 |
| smtinterpol | 0 | 13 | 237033.585 | 233683.716 | 13 | 0 | 13 | 187 | 187 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 30 | 99885.256 | 99888.936 | 30 | 30 | 0 | 70 | 100 | 95 | 0 |
| z3-4.8.17n | 0 | 7 | 115611.475 | 115611.998 | 7 | 7 | 0 | 93 | 100 | 99 | 0 |
| 2021-z3n | 0 | 7 | 116077.194 | 116077.647 | 7 | 7 | 0 | 93 | 100 | 99 | 0 |
| smtinterpol | 0 | 0 | 120000.0 | 120000.0 | 0 | 0 | 0 | 100 | 100 | 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 | 94 | 41016.936 | 41020.505 | 94 | 0 | 94 | 6 | 100 | 99 | 0 |
| 2021-z3n | 0 | 94 | 42831.266 | 42833.757 | 94 | 0 | 94 | 6 | 100 | 99 | 0 |
| cvc5 | 0 | 75 | 65822.573 | 65826.665 | 75 | 0 | 75 | 25 | 100 | 95 | 0 |
| smtinterpol | 0 | 13 | 117033.585 | 113683.716 | 13 | 0 | 13 | 87 | 100 | 187 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2021-z3n | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 200 | 200 | 0 |
| cvc5 | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 200 | 200 | 0 |
| smtinterpol | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 200 | 200 | 0 |
| z3-4.8.17n | 0 | 0 | 4800.0 | 4800.0 | 0 | 0 | 0 | 200 | 200 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.