QF_LIA (Model Validation Track)
Competition results for the QF_LIA
logic
in the Model Validation Track.
Results were generated on 2024-07-08
Benchmarks: 4151
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| cvc5 | cvc5 | cvc5 | - | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 3949 | 76029.352033 | 76436.053251 | 3949 | 3949 | 0 | 202 | 0 | 202 | 0 |
| OpenSMT | 0 | 3949 | 219568.19047 | 220014.935815 | 3949 | 3949 | 0 | 202 | 0 | 201 | 0 |
| Yices2 | 0 | 3823 | 52027.240332 | 52421.363045 | 3823 | 3823 | 0 | 328 | 0 | 328 | 0 |
| SMTInterpol | 0 | 3771 | 138124.384662 | 113142.206733 | 3774 | 3774 | 0 | 377 | 0 | 356 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 3949 | 76029.352033 | 76436.053251 | 3949 | 3949 | 0 | 202 | 0 | 202 | 0 |
| OpenSMT | 0 | 3949 | 219568.19047 | 220014.935815 | 3949 | 3949 | 0 | 202 | 0 | 201 | 0 |
| Yices2 | 0 | 3823 | 52027.240332 | 52421.363045 | 3823 | 3823 | 0 | 328 | 0 | 328 | 0 |
| SMTInterpol | 0 | 3774 | 141865.304632 | 116444.632022 | 3774 | 3774 | 0 | 377 | 0 | 356 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 3949 | 76029.352033 | 76436.053251 | 3949 | 3949 | 0 | 202 | 0 | 202 | 0 |
| OpenSMT | 0 | 3949 | 219568.19047 | 220014.935815 | 3949 | 3949 | 0 | 202 | 0 | 201 | 0 |
| Yices2 | 0 | 3823 | 52027.240332 | 52421.363045 | 3823 | 3823 | 0 | 328 | 0 | 328 | 0 |
| SMTInterpol | 0 | 3774 | 141865.304632 | 116444.632022 | 3774 | 3774 | 0 | 377 | 0 | 356 | 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 | 3643 | 2558.33722 | 2922.387601 | 3643 | 3643 | 0 | 0 | 508 | 0 | 0 |
| cvc5 | 0 | 3353 | 4051.32789 | 4386.26693 | 3353 | 3353 | 0 | 0 | 798 | 0 | 0 |
| SMTInterpol | 0 | 3149 | 15528.497817 | 7102.006896 | 3149 | 3149 | 0 | 0 | 1002 | 0 | 0 |
| OpenSMT | 0 | 3138 | 3766.839777 | 4080.913693 | 3138 | 3138 | 0 | 1 | 1012 | 0 | 0 |