QF_UFLRA (Single Query Track)
Competition results for the QF_UFLRA
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 541
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 | 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 | 539 | 832.19 | 899.15 | 539 | 331 | 208 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 538 | 776.05 | 842.32 | 538 | 330 | 208 | 3 | 0 | 3 | 0 |
| SMTInterpol | 0 | 537 | 3147.77 | 1277.42 | 537 | 330 | 207 | 4 | 0 | 4 | 0 |
| OpenSMT | 0 | 535 | 544.67 | 610.77 | 535 | 327 | 208 | 6 | 0 | 6 | 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 | 539 | 832.19 | 899.15 | 539 | 331 | 208 | 2 | 0 | 2 | 0 |
| cvc5 | 0 | 538 | 776.05 | 842.32 | 538 | 330 | 208 | 3 | 0 | 3 | 0 |
| SMTInterpol | 0 | 537 | 3147.77 | 1277.42 | 537 | 330 | 207 | 4 | 0 | 4 | 0 |
| OpenSMT | 0 | 535 | 544.67 | 610.77 | 535 | 327 | 208 | 6 | 0 | 6 | 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 | 331 | 795.47 | 836.64 | 331 | 331 | 0 | 1 | 209 | 1 | 0 |
| cvc5 | 0 | 330 | 676.02 | 716.69 | 330 | 330 | 0 | 2 | 209 | 2 | 0 |
| SMTInterpol | 0 | 330 | 2133.91 | 847.11 | 330 | 330 | 0 | 2 | 209 | 2 | 0 |
| OpenSMT | 0 | 327 | 482.90 | 523.32 | 327 | 327 | 0 | 5 | 209 | 5 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 208 | 36.71 | 62.51 | 208 | 0 | 208 | 0 | 333 | 0 | 0 |
| OpenSMT | 0 | 208 | 61.76 | 87.45 | 208 | 0 | 208 | 0 | 333 | 0 | 0 |
| cvc5 | 0 | 208 | 100.04 | 125.63 | 208 | 0 | 208 | 0 | 333 | 0 | 0 |
| SMTInterpol | 0 | 207 | 1013.86 | 430.31 | 207 | 0 | 207 | 1 | 333 | 1 | 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 | 538 | 106.30 | 173.07 | 538 | 330 | 208 | 0 | 3 | 0 | 0 |
| cvc5 | 0 | 533 | 170.83 | 236.42 | 533 | 326 | 207 | 0 | 8 | 0 | 0 |
| SMTInterpol | 0 | 532 | 1993.53 | 807.46 | 532 | 326 | 206 | 0 | 9 | 0 | 0 |
| OpenSMT | 0 | 530 | 306.74 | 372.17 | 530 | 322 | 208 | 0 | 11 | 0 | 0 |