QF_ALIA (Single Query Track)
Competition results for the QF_ALIA
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 176
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| SMTInterpol | SMTInterpol | SMTInterpol | Yices2 | SMTInterpol |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 170 | 1516.56 | 971.92 | 170 | 98 | 72 | 6 | 0 | 0 | 0 |
| Yices2 | 0 | 161 | 707.23 | 727.26 | 161 | 89 | 72 | 15 | 0 | 15 | 0 |
| OpenSMT | 0 | 158 | 4468.22 | 4488.35 | 158 | 86 | 72 | 18 | 0 | 18 | 0 |
| cvc5 | 0 | 156 | 4590.23 | 4610.17 | 156 | 85 | 71 | 20 | 0 | 20 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 170 | 1516.56 | 971.92 | 170 | 98 | 72 | 6 | 0 | 0 | 0 |
| Yices2 | 0 | 161 | 707.23 | 727.26 | 161 | 89 | 72 | 15 | 0 | 15 | 0 |
| OpenSMT | 0 | 158 | 4468.22 | 4488.35 | 158 | 86 | 72 | 18 | 0 | 18 | 0 |
| cvc5 | 0 | 156 | 4590.23 | 4610.17 | 156 | 85 | 71 | 20 | 0 | 20 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 98 | 978.45 | 639.29 | 98 | 98 | 0 | 2 | 76 | 0 | 0 |
| Yices2 | 0 | 89 | 692.45 | 703.55 | 89 | 89 | 0 | 11 | 76 | 11 | 0 |
| OpenSMT | 0 | 86 | 4141.42 | 4152.60 | 86 | 86 | 0 | 14 | 76 | 14 | 0 |
| cvc5 | 0 | 85 | 3057.01 | 3067.91 | 85 | 85 | 0 | 15 | 76 | 15 | 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 | 72 | 14.78 | 23.70 | 72 | 0 | 72 | 0 | 104 | 0 | 0 |
| SMTInterpol | 0 | 72 | 538.11 | 332.63 | 72 | 0 | 72 | 0 | 104 | 0 | 0 |
| OpenSMT | 0 | 72 | 326.80 | 335.76 | 72 | 0 | 72 | 0 | 104 | 0 | 0 |
| cvc5 | 0 | 71 | 1533.21 | 1542.26 | 71 | 0 | 71 | 1 | 104 | 1 | 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 |
|---|
| SMTInterpol | 0 | 161 | 756.92 | 330.58 | 161 | 92 | 69 | 4 | 11 | 0 | 0 |
| Yices2 | 0 | 160 | 82.51 | 102.35 | 160 | 88 | 72 | 0 | 16 | 0 | 0 |
| cvc5 | 0 | 135 | 272.55 | 289.19 | 135 | 70 | 65 | 0 | 41 | 0 | 0 |
| OpenSMT | 0 | 123 | 240.06 | 255.24 | 123 | 54 | 69 | 0 | 53 | 0 | 0 |