QF_LIA (Model Validation Track)
Competition results for the QF_LIA
logic
in the Model Validation Track. Chart
Results were generated on 2025-08-11
Benchmarks: 4158
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | OpenSMT | OpenSMT | - | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 3975 | 197961.09 | 198484.77 | 3975 | 3975 | 183 | 0 | 183 | 0 |
| Yices2 | 0 | 3870 | 44188.31 | 44669.80 | 3870 | 3870 | 288 | 0 | 288 | 0 |
| SMTInterpol | 0 | 3715 | 118582.31 | 97797.95 | 3717 | 3717 | 441 | 0 | 437 | 0 |
| cvc5 | 0 | 3220 | 121367.70 | 121779.75 | 3220 | 3220 | 938 | 0 | 938 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 3975 | 197961.09 | 198484.77 | 3975 | 3975 | 183 | 0 | 183 | 0 |
| Yices2 | 0 | 3870 | 44188.31 | 44669.80 | 3870 | 3870 | 288 | 0 | 288 | 0 |
| SMTInterpol | 0 | 3717 | 121099.59 | 99881.17 | 3717 | 3717 | 441 | 0 | 437 | 0 |
| cvc5 | 0 | 3220 | 121367.70 | 121779.75 | 3220 | 3220 | 938 | 0 | 938 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 3975 | 197961.09 | 198484.77 | 3975 | 3975 | 183 | 0 | 183 | 0 |
| Yices2 | 0 | 3870 | 44188.31 | 44669.80 | 3870 | 3870 | 288 | 0 | 288 | 0 |
| SMTInterpol | 0 | 3717 | 121099.59 | 99881.17 | 3717 | 3717 | 441 | 0 | 437 | 0 |
| cvc5 | 0 | 3220 | 121367.70 | 121779.75 | 3220 | 3220 | 938 | 0 | 938 | 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 | 3708 | 2488.02 | 2944.32 | 3708 | 3708 | 0 | 450 | 0 | 0 |
| OpenSMT | 0 | 3210 | 4131.54 | 4527.03 | 3210 | 3210 | 0 | 948 | 0 | 0 |
| SMTInterpol | 0 | 3126 | 12618.86 | 6188.19 | 3126 | 3126 | 0 | 1032 | 0 | 0 |
| cvc5 | 0 | 2931 | 2633.73 | 2990.75 | 2931 | 2931 | 0 | 1227 | 0 | 0 |