The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_IDL logic in the Model Validation Track.
Page generated on 2023-07-06 16:06:00 +0000
Benchmarks: 745 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance |
|---|---|
| Z3++ | Z3++ |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| 2022-Z3++n | 0 | 688 | 45228.632 | 45250.807 | 53 | 0 |
| Z3++ | 0 | 688 | 45725.406 | 45715.266 | 53 | 0 |
| Yices2 | 0 | 651 | 20309.999 | 20282.892 | 91 | 0 |
| OpenSMT | 0 | 591 | 54840.284 | 54760.706 | 150 | 0 |
| cvc5 | 0 | 568 | 57840.538 | 57842.785 | 173 | 0 |
| SMTInterpol | 0 | 446 | 65590.603 | 59671.46 | 295 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| 2022-Z3++n | 0 | 688 | 45228.632 | 45250.807 | 53 | 0 |
| Z3++ | 0 | 688 | 45725.406 | 45715.266 | 53 | 0 |
| Yices2 | 0 | 651 | 20309.999 | 20282.892 | 91 | 0 |
| OpenSMT | 0 | 591 | 54840.284 | 54760.706 | 150 | 0 |
| cvc5 | 0 | 568 | 57840.538 | 57842.785 | 173 | 0 |
| SMTInterpol | 0 | 448 | 68021.243 | 62013.8 | 293 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.