QF_LRA (Single Query Track)
Competition results for the QF_LRA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 595
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | OpenSMT | OpenSMT | OpenSMT | OpenSMT |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 574 | 19727.558409 | 19789.987929 | 574 | 327 | 247 | 21 | 0 | 21 | 0 |
| cvc5 | 0 | 552 | 35265.793893 | 35328.701852 | 552 | 312 | 240 | 43 | 0 | 43 | 0 |
| Z3-alpha | 0 | 550 | 28636.302666 | 28697.880915 | 550 | 315 | 235 | 45 | 0 | 45 | 0 |
| Yices2 | 0 | 549 | 25861.297788 | 25922.952445 | 549 | 316 | 233 | 46 | 0 | 46 | 0 |
| SMTInterpol | 0 | 510 | 62756.560165 | 53029.582481 | 516 | 307 | 209 | 79 | 0 | 79 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 574 | 19727.558409 | 19789.987929 | 574 | 327 | 247 | 21 | 0 | 21 | 0 |
| cvc5 | 0 | 552 | 35265.793893 | 35328.701852 | 552 | 312 | 240 | 43 | 0 | 43 | 0 |
| Z3-alpha | 0 | 550 | 28636.302666 | 28697.880915 | 550 | 315 | 235 | 45 | 0 | 45 | 0 |
| Yices2 | 0 | 549 | 25861.297788 | 25922.952445 | 549 | 316 | 233 | 46 | 0 | 46 | 0 |
| SMTInterpol | 0 | 516 | 71094.732207 | 58876.559731 | 516 | 307 | 209 | 79 | 0 | 79 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 327 | 13443.238943 | 13479.144539 | 327 | 327 | 0 | 9 | 259 | 9 | 0 |
| Yices2 | 0 | 316 | 8917.600217 | 8950.822824 | 316 | 316 | 0 | 20 | 259 | 20 | 0 |
| Z3-alpha | 0 | 315 | 15640.807319 | 15676.198789 | 315 | 315 | 0 | 21 | 259 | 21 | 0 |
| cvc5 | 0 | 312 | 21085.692588 | 21121.529542 | 312 | 312 | 0 | 24 | 259 | 24 | 0 |
| SMTInterpol | 0 | 307 | 35004.451328 | 28649.600577 | 307 | 307 | 0 | 29 | 259 | 29 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 247 | 6284.319466 | 6310.84339 | 247 | 0 | 247 | 6 | 342 | 6 | 0 |
| cvc5 | 0 | 240 | 14180.101305 | 14207.17231 | 240 | 0 | 240 | 13 | 342 | 13 | 0 |
| Z3-alpha | 0 | 235 | 12995.495347 | 13021.682126 | 235 | 0 | 235 | 18 | 342 | 18 | 0 |
| Yices2 | 0 | 233 | 16943.697571 | 16972.129621 | 233 | 0 | 233 | 20 | 342 | 20 | 0 |
| SMTInterpol | 0 | 209 | 36090.28088 | 30226.959154 | 209 | 0 | 209 | 44 | 342 | 44 | 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 |
|---|
| OpenSMT | 0 | 470 | 1580.602067 | 1628.454294 | 470 | 264 | 206 | 0 | 125 | 0 | 0 |
| Yices2 | 0 | 458 | 1207.163255 | 1253.303257 | 458 | 284 | 174 | 0 | 137 | 0 | 0 |
| Z3-alpha | 0 | 392 | 1288.320502 | 1327.846918 | 392 | 219 | 173 | 0 | 203 | 0 | 0 |
| cvc5 | 0 | 365 | 1102.017262 | 1138.829311 | 365 | 207 | 158 | 0 | 230 | 0 | 0 |
| SMTInterpol | 0 | 314 | 3065.071636 | 1289.916035 | 314 | 199 | 115 | 0 | 281 | 0 | 0 |