QF_IDL (Model Validation Track)
Competition results for the QF_IDL
logic
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 736
Time Limit: 1200 seconds
Memory Limit: 20480 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 | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 659 | 21444.429825 | 21513.705346 | 659 | 659 | 0 | 77 | 0 | 73 | 0 |
| OpenSMT | 0 | 602 | 39754.291196 | 39825.357227 | 602 | 602 | 0 | 134 | 0 | 134 | 0 |
| cvc5 | 0 | 578 | 50702.469234 | 50768.328615 | 578 | 578 | 0 | 158 | 0 | 156 | 2 |
| SMTInterpol | 0 | 459 | 60058.753708 | 50506.235285 | 464 | 464 | 0 | 272 | 0 | 272 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 659 | 21444.429825 | 21513.705346 | 659 | 659 | 0 | 77 | 0 | 73 | 0 |
| OpenSMT | 0 | 602 | 39754.291196 | 39825.357227 | 602 | 602 | 0 | 134 | 0 | 134 | 0 |
| cvc5 | 0 | 578 | 50702.469234 | 50768.328615 | 578 | 578 | 0 | 158 | 0 | 156 | 2 |
| SMTInterpol | 0 | 464 | 68759.874432 | 54187.535838 | 464 | 464 | 0 | 272 | 0 | 272 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 659 | 21444.429825 | 21513.705346 | 659 | 659 | 0 | 77 | 0 | 73 | 0 |
| OpenSMT | 0 | 602 | 39754.291196 | 39825.357227 | 602 | 602 | 0 | 134 | 0 | 134 | 0 |
| cvc5 | 0 | 578 | 50702.469234 | 50768.328615 | 578 | 578 | 0 | 158 | 0 | 156 | 2 |
| SMTInterpol | 0 | 464 | 68759.874432 | 54187.535838 | 464 | 464 | 0 | 272 | 0 | 272 | 0 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 582 | 866.357909 | 924.637287 | 582 | 582 | 0 | 0 | 154 | 0 | 0 |
| OpenSMT | 0 | 375 | 1410.253972 | 1448.040496 | 375 | 375 | 0 | 0 | 361 | 0 | 0 |
| cvc5 | 0 | 356 | 1417.88471 | 1453.634636 | 356 | 356 | 0 | 0 | 380 | 0 | 0 |
| SMTInterpol | 0 | 282 | 3577.37602 | 1579.472618 | 282 | 282 | 0 | 0 | 454 | 0 | 0 |