QF_LRA (Model Validation Track)
Competition results for the QF_LRA
logic
in the Model Validation Track. Chart
Results were generated on 2025-08-11
Benchmarks: 497
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 | - | OpenSMT |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 483 | 12202.81 | 12264.44 | 483 | 483 | 14 | 0 | 14 | 0 |
| Yices2 | 0 | 482 | 11352.44 | 11413.04 | 482 | 482 | 15 | 0 | 15 | 0 |
| SMTInterpol | 0 | 445 | 26853.58 | 23713.99 | 445 | 445 | 52 | 0 | 52 | 0 |
| cvc5 | 0 | 366 | 2309.06 | 2353.44 | 366 | 366 | 131 | 0 | 131 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 483 | 12202.81 | 12264.44 | 483 | 483 | 14 | 0 | 14 | 0 |
| Yices2 | 0 | 482 | 11352.44 | 11413.04 | 482 | 482 | 15 | 0 | 15 | 0 |
| SMTInterpol | 0 | 445 | 26853.58 | 23713.99 | 445 | 445 | 52 | 0 | 52 | 0 |
| cvc5 | 0 | 366 | 2309.06 | 2353.44 | 366 | 366 | 131 | 0 | 131 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 483 | 12202.81 | 12264.44 | 483 | 483 | 14 | 0 | 14 | 0 |
| Yices2 | 0 | 482 | 11352.44 | 11413.04 | 482 | 482 | 15 | 0 | 15 | 0 |
| SMTInterpol | 0 | 445 | 26853.58 | 23713.99 | 445 | 445 | 52 | 0 | 52 | 0 |
| cvc5 | 0 | 366 | 2309.06 | 2353.44 | 366 | 366 | 131 | 0 | 131 | 0 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 433 | 932.36 | 985.89 | 433 | 433 | 0 | 64 | 0 | 0 |
| Yices2 | 0 | 431 | 587.37 | 640.34 | 431 | 431 | 0 | 66 | 0 | 0 |
| SMTInterpol | 0 | 355 | 1973.33 | 914.71 | 355 | 355 | 0 | 142 | 0 | 0 |
| cvc5 | 0 | 351 | 404.10 | 446.47 | 351 | 351 | 0 | 146 | 0 | 0 |