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.