QF_LIA (Single Query Track)
Competition results for the QF_LIA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 4825
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 | SMTInterpol | 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 | 4514 | 285099.354098 | 285624.183105 | 4514 | 2749 | 1765 | 311 | 0 | 301 | 0 |
| cvc5 | 0 | 4450 | 221746.09636 | 222243.563191 | 4450 | 2726 | 1724 | 375 | 0 | 368 | 0 |
| Yices2 | 0 | 4364 | 64155.389351 | 64605.357102 | 4364 | 2649 | 1715 | 461 | 0 | 445 | 10 |
| SMTInterpol | 0 | 4330 | 244233.870279 | 178152.16742 | 4340 | 2571 | 1769 | 485 | 0 | 479 | 0 |
| Z3-alpha | 0 | 4169 | 183171.504142 | 183628.955591 | 4169 | 2686 | 1483 | 656 | 0 | 610 | 39 |
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 | 4514 | 285099.354098 | 285624.183105 | 4514 | 2749 | 1765 | 311 | 0 | 301 | 0 |
| cvc5 | 0 | 4450 | 221746.09636 | 222243.563191 | 4450 | 2726 | 1724 | 375 | 0 | 368 | 0 |
| Yices2 | 0 | 4364 | 64155.389351 | 64605.357102 | 4364 | 2649 | 1715 | 461 | 0 | 445 | 10 |
| SMTInterpol | 0 | 4340 | 259428.907094 | 188195.530205 | 4340 | 2571 | 1769 | 485 | 0 | 479 | 0 |
| Z3-alpha | 0 | 4169 | 183171.504142 | 183628.955591 | 4169 | 2686 | 1483 | 656 | 0 | 610 | 39 |
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 | 2749 | 209159.155265 | 209487.046595 | 2749 | 2749 | 0 | 210 | 1866 | 209 | 0 |
| cvc5 | 0 | 2726 | 108962.217812 | 109261.192553 | 2726 | 2726 | 0 | 233 | 1866 | 233 | 0 |
| Z3-alpha | 0 | 2686 | 98568.630998 | 98858.307307 | 2686 | 2686 | 0 | 273 | 1866 | 268 | 4 |
| Yices2 | 0 | 2649 | 54092.359999 | 54369.02346 | 2649 | 2649 | 0 | 310 | 1866 | 310 | 0 |
| SMTInterpol | 0 | 2571 | 149904.547111 | 119887.702685 | 2571 | 2571 | 0 | 388 | 1866 | 388 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 1769 | 109524.359982 | 68307.82752 | 1769 | 0 | 1769 | 55 | 3001 | 55 | 0 |
| OpenSMT | 0 | 1765 | 75940.198832 | 76137.136511 | 1765 | 0 | 1765 | 59 | 3001 | 56 | 0 |
| cvc5 | 0 | 1724 | 112783.878548 | 112982.370638 | 1724 | 0 | 1724 | 100 | 3001 | 99 | 0 |
| Yices2 | 0 | 1715 | 10063.029352 | 10236.333642 | 1715 | 0 | 1715 | 109 | 3001 | 109 | 0 |
| Z3-alpha | 0 | 1483 | 84602.873144 | 84770.648284 | 1483 | 0 | 1483 | 341 | 3001 | 317 | 24 |
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 | 4164 | 3691.746636 | 4108.29585 | 4164 | 2477 | 1687 | 6 | 655 | 0 | 0 |
| Z3-alpha | 0 | 3295 | 4762.56805 | 5092.059331 | 3295 | 2243 | 1052 | 6 | 1524 | 0 | 0 |
| OpenSMT | 0 | 3239 | 8349.887879 | 8675.398467 | 3239 | 1959 | 1280 | 10 | 1576 | 0 | 0 |
| cvc5 | 0 | 3136 | 5670.194205 | 5984.208658 | 3136 | 2043 | 1093 | 6 | 1683 | 0 | 0 |
| SMTInterpol | 0 | 3067 | 26646.402122 | 11314.590099 | 3067 | 1956 | 1111 | 6 | 1752 | 0 | 0 |