QF_LinearRealArith (Single Query Track)
Competition results for the QF_LinearRealArith
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 842
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | OpenSMT | OpenSMT | cvc5 | Yices2 |
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 | 768 | 33545.690415 | 33630.000387 | 768 | 427 | 341 | 74 | 0 | 74 | 0 |
| Yices2 | 0 | 762 | 27377.968764 | 27461.27648 | 762 | 421 | 341 | 80 | 0 | 80 | 0 |
| cvc5 | 0 | 761 | 42308.879871 | 42393.932934 | 761 | 414 | 347 | 81 | 0 | 81 | 0 |
| Z3-alpha | 0 | 757 | 33484.733606 | 33568.181297 | 757 | 414 | 343 | 85 | 0 | 66 | 0 |
| SMTInterpol | 0 | 692 | 75446.567669 | 62160.040553 | 698 | 408 | 290 | 144 | 0 | 142 | 2 |
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 | 768 | 33545.690415 | 33630.000387 | 768 | 427 | 341 | 74 | 0 | 74 | 0 |
| Yices2 | 0 | 762 | 27377.968764 | 27461.27648 | 762 | 421 | 341 | 80 | 0 | 80 | 0 |
| cvc5 | 0 | 761 | 42308.879871 | 42393.932934 | 761 | 414 | 347 | 81 | 0 | 81 | 0 |
| Z3-alpha | 0 | 757 | 33484.733606 | 33568.181297 | 757 | 414 | 343 | 85 | 0 | 66 | 0 |
| SMTInterpol | 0 | 698 | 83784.739711 | 68007.017804 | 698 | 408 | 290 | 144 | 0 | 142 | 2 |
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 | 427 | 20625.318092 | 20672.182167 | 427 | 427 | 0 | 14 | 401 | 14 | 0 |
| Yices2 | 0 | 421 | 9299.691354 | 9343.541607 | 421 | 421 | 0 | 20 | 401 | 20 | 0 |
| Z3-alpha | 0 | 414 | 18495.467108 | 18541.552067 | 414 | 414 | 0 | 27 | 401 | 27 | 0 |
| cvc5 | 0 | 414 | 23798.113936 | 23844.662973 | 414 | 414 | 0 | 27 | 401 | 27 | 0 |
| SMTInterpol | 0 | 408 | 41514.657517 | 34133.809555 | 408 | 408 | 0 | 33 | 401 | 33 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 347 | 18510.765935 | 18549.269962 | 347 | 0 | 347 | 15 | 480 | 15 | 0 |
| Z3-alpha | 0 | 343 | 14989.266497 | 15026.62923 | 343 | 0 | 343 | 19 | 480 | 19 | 0 |
| OpenSMT | 0 | 341 | 12920.372324 | 12957.81822 | 341 | 0 | 341 | 21 | 480 | 21 | 0 |
| Yices2 | 0 | 341 | 18078.277409 | 18117.734873 | 341 | 0 | 341 | 21 | 480 | 21 | 0 |
| SMTInterpol | 0 | 290 | 42270.082194 | 33873.208249 | 290 | 0 | 290 | 72 | 480 | 70 | 2 |
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 | 653 | 1546.011944 | 1611.71718 | 653 | 383 | 270 | 0 | 189 | 0 | 0 |
| OpenSMT | 0 | 617 | 1939.374922 | 2002.130433 | 617 | 344 | 273 | 0 | 225 | 0 | 0 |
| Z3-alpha | 0 | 575 | 1805.728936 | 1863.681289 | 575 | 309 | 266 | 19 | 248 | 0 | 0 |
| cvc5 | 0 | 535 | 1688.738306 | 1742.698463 | 535 | 295 | 240 | 0 | 307 | 0 | 0 |
| SMTInterpol | 0 | 450 | 4815.942746 | 2059.487315 | 450 | 274 | 176 | 0 | 392 | 0 | 0 |