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 |