The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_AUFLIA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 530 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
| 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 | 530 | 17.024 | 16.151 | 530 | 273 | 257 | 0 | 0 | 0 |
| Yices2 | 0 | 530 | 20.38 | 21.725 | 530 | 273 | 257 | 0 | 0 | 0 |
| cvc5 | 0 | 530 | 223.428 | 223.39 | 530 | 273 | 257 | 0 | 0 | 0 |
| OpenSMT | 0 | 530 | 319.563 | 320.086 | 530 | 273 | 257 | 0 | 0 | 0 |
| SMTInterpol | 0 | 530 | 1130.002 | 495.89 | 530 | 273 | 257 | 0 | 0 | 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 | 530 | 17.024 | 16.151 | 530 | 273 | 257 | 0 | 0 | 0 |
| Yices2 | 0 | 530 | 20.38 | 21.725 | 530 | 273 | 257 | 0 | 0 | 0 |
| cvc5 | 0 | 530 | 223.428 | 223.39 | 530 | 273 | 257 | 0 | 0 | 0 |
| OpenSMT | 0 | 530 | 319.563 | 320.086 | 530 | 273 | 257 | 0 | 0 | 0 |
| SMTInterpol | 0 | 530 | 1130.002 | 495.89 | 530 | 273 | 257 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 273 | 4.525 | 5.42 | 273 | 273 | 0 | 0 | 257 | 0 | 0 |
| 2022-z3-4.8.17n | 0 | 273 | 6.356 | 5.905 | 273 | 273 | 0 | 0 | 257 | 0 | 0 |
| cvc5 | 0 | 273 | 120.414 | 120.392 | 273 | 273 | 0 | 0 | 257 | 0 | 0 |
| OpenSMT | 0 | 273 | 138.214 | 138.515 | 273 | 273 | 0 | 0 | 257 | 0 | 0 |
| SMTInterpol | 0 | 273 | 306.905 | 152.779 | 273 | 273 | 0 | 0 | 257 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-z3-4.8.17n | 0 | 257 | 10.668 | 10.246 | 257 | 0 | 257 | 0 | 273 | 0 | 0 |
| Yices2 | 0 | 257 | 15.855 | 16.304 | 257 | 0 | 257 | 0 | 273 | 0 | 0 |
| cvc5 | 0 | 257 | 103.014 | 102.998 | 257 | 0 | 257 | 0 | 273 | 0 | 0 |
| OpenSMT | 0 | 257 | 181.349 | 181.571 | 257 | 0 | 257 | 0 | 273 | 0 | 0 |
| SMTInterpol | 0 | 257 | 823.097 | 343.111 | 257 | 0 | 257 | 0 | 273 | 0 | 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 | 530 | 17.024 | 16.151 | 530 | 273 | 257 | 0 | 0 | 0 |
| Yices2 | 0 | 530 | 20.38 | 21.725 | 530 | 273 | 257 | 0 | 0 | 0 |
| OpenSMT | 0 | 530 | 319.563 | 320.086 | 530 | 273 | 257 | 0 | 0 | 0 |
| SMTInterpol | 0 | 530 | 1130.002 | 495.89 | 530 | 273 | 257 | 0 | 0 | 0 |
| cvc5 | 0 | 529 | 192.818 | 192.775 | 529 | 273 | 256 | 1 | 1 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.