QF_UFLRA (Single Query Track)
Competition results for the QF_UFLRA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 541
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 | 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 | 538 | 153.003173 | 206.821189 | 538 | 333 | 205 | 3 | 0 | 3 | 0 |
| cvc5 | 0 | 536 | 1172.14896 | 1225.736659 | 536 | 331 | 205 | 5 | 0 | 5 | 0 |
| SMTInterpol | 0 | 536 | 4248.160039 | 1788.708304 | 536 | 333 | 203 | 5 | 0 | 5 | 0 |
| OpenSMT | 0 | 534 | 1986.768772 | 2040.498072 | 534 | 329 | 205 | 7 | 0 | 7 | 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 | 538 | 153.003173 | 206.821189 | 538 | 333 | 205 | 3 | 0 | 3 | 0 |
| cvc5 | 0 | 536 | 1172.14896 | 1225.736659 | 536 | 331 | 205 | 5 | 0 | 5 | 0 |
| SMTInterpol | 0 | 536 | 4248.160039 | 1788.708304 | 536 | 333 | 203 | 5 | 0 | 5 | 0 |
| OpenSMT | 0 | 534 | 1986.768772 | 2040.498072 | 534 | 329 | 205 | 7 | 0 | 7 | 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 | 333 | 119.231802 | 152.542224 | 333 | 333 | 0 | 2 | 206 | 2 | 0 |
| SMTInterpol | 0 | 333 | 3178.953136 | 1397.143171 | 333 | 333 | 0 | 2 | 206 | 2 | 0 |
| cvc5 | 0 | 331 | 1016.351143 | 1049.477259 | 331 | 331 | 0 | 4 | 206 | 4 | 0 |
| OpenSMT | 0 | 329 | 1894.5379 | 1927.718089 | 329 | 329 | 0 | 6 | 206 | 6 | 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 | 205 | 33.77137 | 54.278966 | 205 | 0 | 205 | 0 | 336 | 0 | 0 |
| OpenSMT | 0 | 205 | 92.230872 | 112.779983 | 205 | 0 | 205 | 0 | 336 | 0 | 0 |
| cvc5 | 0 | 205 | 155.797817 | 176.2594 | 205 | 0 | 205 | 0 | 336 | 0 | 0 |
| SMTInterpol | 0 | 203 | 1069.206903 | 391.565132 | 203 | 0 | 203 | 2 | 336 | 2 | 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 | 536 | 94.163362 | 147.774495 | 536 | 331 | 205 | 0 | 5 | 0 | 0 |
| cvc5 | 0 | 532 | 157.074504 | 210.144648 | 532 | 329 | 203 | 0 | 9 | 0 | 0 |
| SMTInterpol | 0 | 532 | 2305.496358 | 864.319388 | 532 | 329 | 203 | 0 | 9 | 0 | 0 |
| OpenSMT | 0 | 522 | 313.835751 | 366.091761 | 522 | 319 | 203 | 0 | 19 | 0 | 0 |