The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFBVDTLIA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:53 +0000
Benchmarks: 742 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 337 | 61125.94 | 64811.712 | 337 | 174 | 163 | 405 | 364 | 0 |
| 2022-z3-4.8.17n | 0 | 155 | 3337.999 | 3338.081 | 155 | 58 | 97 | 587 | 545 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 2 | 23.17 | 8.741 | 2 | 0 | 2 | 740 | 17 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 337 | 61125.94 | 64811.712 | 337 | 174 | 163 | 405 | 364 | 0 |
| 2022-z3-4.8.17n | 0 | 155 | 3337.999 | 3338.081 | 155 | 58 | 97 | 587 | 545 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 2 | 23.17 | 8.741 | 2 | 0 | 2 | 740 | 17 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 174 | 39246.271 | 42152.261 | 174 | 174 | 0 | 3 | 565 | 364 | 0 |
| 2022-z3-4.8.17n | 0 | 58 | 3305.177 | 3305.442 | 58 | 58 | 0 | 119 | 565 | 545 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 177 | 565 | 17 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 163 | 21879.668 | 22659.45 | 163 | 0 | 163 | 0 | 579 | 364 | 0 |
| 2022-z3-4.8.17n | 0 | 97 | 32.822 | 32.639 | 97 | 0 | 97 | 66 | 579 | 545 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 2 | 23.17 | 8.741 | 2 | 0 | 2 | 161 | 579 | 17 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-z3-4.8.17n | 0 | 149 | 73.611 | 73.344 | 149 | 52 | 97 | 593 | 585 | 0 |
| cvc5 | 0 | 106 | 33.132 | 33.69 | 106 | 6 | 100 | 636 | 636 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 2 | 23.17 | 8.741 | 2 | 0 | 2 | 740 | 20 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.