QF_IDL (Model Validation Track)
Competition results for the QF_IDL
logic
in the Model Validation Track. Chart
Results were generated on 2025-08-11
Benchmarks: 736
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Yices2 | Yices2 | Yices2 | - | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 663 | 18100.18 | 18183.75 | 663 | 663 | 73 | 0 | 72 | 0 |
| OpenSMT | 0 | 608 | 40013.70 | 40094.30 | 608 | 608 | 128 | 0 | 128 | 0 |
| cvc5 | 0 | 594 | 49413.12 | 49493.03 | 594 | 594 | 142 | 0 | 138 | 4 |
| SMTInterpol | 0 | 380 | 26144.56 | 22160.38 | 380 | 380 | 356 | 0 | 208 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 663 | 18100.18 | 18183.75 | 663 | 663 | 73 | 0 | 72 | 0 |
| OpenSMT | 0 | 608 | 40013.70 | 40094.30 | 608 | 608 | 128 | 0 | 128 | 0 |
| cvc5 | 0 | 594 | 49413.12 | 49493.03 | 594 | 594 | 142 | 0 | 138 | 4 |
| SMTInterpol | 0 | 380 | 26144.56 | 22160.38 | 380 | 380 | 356 | 0 | 208 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 663 | 18100.18 | 18183.75 | 663 | 663 | 73 | 0 | 72 | 0 |
| OpenSMT | 0 | 608 | 40013.70 | 40094.30 | 608 | 608 | 128 | 0 | 128 | 0 |
| cvc5 | 0 | 594 | 49413.12 | 49493.03 | 594 | 594 | 142 | 0 | 138 | 4 |
| SMTInterpol | 0 | 380 | 26144.56 | 22160.38 | 380 | 380 | 356 | 0 | 208 | 0 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 599 | 936.64 | 1009.93 | 599 | 599 | 1 | 136 | 0 | 0 |
| OpenSMT | 0 | 411 | 1373.16 | 1423.91 | 411 | 411 | 0 | 325 | 0 | 0 |
| cvc5 | 0 | 388 | 1253.53 | 1301.08 | 388 | 388 | 0 | 348 | 0 | 0 |
| SMTInterpol | 0 | 272 | 2750.85 | 1300.92 | 272 | 272 | 120 | 344 | 0 | 0 |