QF_LIRA (Single Query Track)
Competition results for the QF_LIRA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 7
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Z3-alpha | Z3-alpha | Yices2 | Z3-alpha | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 6 | 93.72383 | 94.345589 | 6 | 1 | 5 | 1 | 0 | 1 | 0 |
| Yices2 | 0 | 6 | 204.532223 | 205.298702 | 6 | 1 | 5 | 1 | 0 | 1 | 0 |
| cvc5 | 0 | 5 | 11.749475 | 12.252042 | 5 | 1 | 4 | 2 | 0 | 2 | 0 |
| SMTInterpol | 0 | 4 | 304.985006 | 184.112201 | 4 | 1 | 3 | 3 | 0 | 3 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 6 | 93.72383 | 94.345589 | 6 | 1 | 5 | 1 | 0 | 1 | 0 |
| Yices2 | 0 | 6 | 204.532223 | 205.298702 | 6 | 1 | 5 | 1 | 0 | 1 | 0 |
| cvc5 | 0 | 5 | 11.749475 | 12.252042 | 5 | 1 | 4 | 2 | 0 | 2 | 0 |
| SMTInterpol | 0 | 4 | 304.985006 | 184.112201 | 4 | 1 | 3 | 3 | 0 | 3 | 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 | 1 | 0.191561 | 0.291198 | 1 | 1 | 0 | 0 | 6 | 0 | 0 |
| Z3-alpha | 0 | 1 | 2.569672 | 2.670766 | 1 | 1 | 0 | 0 | 6 | 0 | 0 |
| cvc5 | 0 | 1 | 3.041584 | 3.14168 | 1 | 1 | 0 | 0 | 6 | 0 | 0 |
| SMTInterpol | 0 | 1 | 20.716899 | 7.491912 | 1 | 1 | 0 | 0 | 6 | 0 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-alpha | 0 | 5 | 91.154158 | 91.674823 | 5 | 0 | 5 | 0 | 2 | 0 | 0 |
| Yices2 | 0 | 5 | 204.340662 | 205.007503 | 5 | 0 | 5 | 0 | 2 | 0 | 0 |
| cvc5 | 0 | 4 | 8.707892 | 9.110362 | 4 | 0 | 4 | 1 | 2 | 1 | 0 |
| SMTInterpol | 0 | 3 | 284.268107 | 176.62029 | 3 | 0 | 3 | 2 | 2 | 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 | 5 | 1.026506 | 1.525136 | 5 | 1 | 4 | 0 | 2 | 0 | 0 |
| Z3-alpha | 0 | 5 | 8.201275 | 8.701012 | 5 | 1 | 4 | 0 | 2 | 0 | 0 |
| cvc5 | 0 | 5 | 11.749475 | 12.252042 | 5 | 1 | 4 | 0 | 2 | 0 | 0 |
| SMTInterpol | 0 | 3 | 42.634999 | 14.796321 | 3 | 1 | 2 | 0 | 4 | 0 | 0 |