The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UF logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 3478 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-Yices2n | 0 | 3478 | 642.547 | 647.705 | 3478 | 1458 | 2020 | 0 | 0 | 0 |
| Yices2 | 0 | 3478 | 673.35 | 674.014 | 3478 | 1458 | 2020 | 0 | 0 | 0 |
| OpenSMT | 0 | 3478 | 6192.099 | 6127.864 | 3478 | 1458 | 2020 | 0 | 0 | 0 |
| cvc5 | 0 | 3476 | 5095.781 | 5076.92 | 3476 | 1458 | 2018 | 2 | 2 | 0 |
| SMTInterpol | 0 | 3407 | 31143.339 | 14856.182 | 3407 | 1458 | 1949 | 71 | 71 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 3478 | 642.547 | 647.705 | 3478 | 1458 | 2020 | 0 | 0 | 0 |
| Yices2 | 0 | 3478 | 673.35 | 674.014 | 3478 | 1458 | 2020 | 0 | 0 | 0 |
| OpenSMT | 0 | 3478 | 6192.099 | 6127.864 | 3478 | 1458 | 2020 | 0 | 0 | 0 |
| cvc5 | 0 | 3476 | 5095.781 | 5076.92 | 3476 | 1458 | 2018 | 2 | 2 | 0 |
| SMTInterpol | 0 | 3414 | 43593.849 | 21162.491 | 3414 | 1458 | 1956 | 64 | 64 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 1458 | 60.111 | 62.548 | 1458 | 1458 | 0 | 0 | 2020 | 0 | 0 |
| Yices2 | 0 | 1458 | 60.873 | 63.392 | 1458 | 1458 | 0 | 0 | 2020 | 0 | 0 |
| OpenSMT | 0 | 1458 | 331.51 | 330.809 | 1458 | 1458 | 0 | 0 | 2020 | 0 | 0 |
| cvc5 | 0 | 1458 | 528.828 | 523.759 | 1458 | 1458 | 0 | 0 | 2020 | 2 | 0 |
| SMTInterpol | 0 | 1458 | 4211.637 | 1676.199 | 1458 | 1458 | 0 | 0 | 2020 | 64 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 2020 | 582.437 | 585.157 | 2020 | 0 | 2020 | 0 | 1458 | 0 | 0 |
| Yices2 | 0 | 2020 | 612.478 | 610.622 | 2020 | 0 | 2020 | 0 | 1458 | 0 | 0 |
| OpenSMT | 0 | 2020 | 5860.589 | 5797.055 | 2020 | 0 | 2020 | 0 | 1458 | 0 | 0 |
| cvc5 | 0 | 2018 | 4566.953 | 4553.16 | 2018 | 0 | 2018 | 2 | 1458 | 2 | 0 |
| SMTInterpol | 0 | 1956 | 39382.212 | 19486.293 | 1956 | 0 | 1956 | 64 | 1458 | 64 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Yices2n | 0 | 3475 | 247.277 | 252.374 | 3475 | 1458 | 2017 | 3 | 3 | 0 |
| Yices2 | 0 | 3475 | 255.178 | 255.749 | 3475 | 1458 | 2017 | 3 | 3 | 0 |
| cvc5 | 0 | 3442 | 1951.184 | 1931.788 | 3442 | 1458 | 1984 | 36 | 36 | 0 |
| OpenSMT | 0 | 3435 | 1798.079 | 1785.768 | 3435 | 1458 | 1977 | 43 | 43 | 0 |
| SMTInterpol | 0 | 3332 | 20923.334 | 8809.928 | 3332 | 1458 | 1874 | 146 | 146 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.