QF_UFLIA (Single Query Track)
Competition results for the QF_UFLIA
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 300
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
|
Yices2
|
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
|
286
|
7153.26 |
5822.20 |
286 |
222 |
64 |
14 |
0 |
14 |
0 |
|
Yices2
|
0
|
283
|
2871.90 |
2907.63 |
283 |
218 |
65 |
17 |
0 |
17 |
0 |
|
cvc5
|
0
|
281
|
1824.45 |
1859.42 |
281 |
217 |
64 |
19 |
0 |
19 |
0 |
|
OpenSMT
|
0
|
278
|
4081.69 |
4116.33 |
278 |
215 |
63 |
22 |
0 |
22 |
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
|
286
|
7153.26 |
5822.20 |
286 |
222 |
64 |
14 |
0 |
14 |
0 |
|
Yices2
|
0
|
283
|
2871.90 |
2907.63 |
283 |
218 |
65 |
17 |
0 |
17 |
0 |
|
cvc5
|
0
|
281
|
1824.45 |
1859.42 |
281 |
217 |
64 |
19 |
0 |
19 |
0 |
|
OpenSMT
|
0
|
278
|
4081.69 |
4116.33 |
278 |
215 |
63 |
22 |
0 |
22 |
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
|
222
|
3321.33 |
2630.59 |
222 |
222 |
0 |
1 |
77 |
1 |
0 |
|
Yices2
|
0
|
218
|
2129.80 |
2157.25 |
218 |
218 |
0 |
5 |
77 |
5 |
0 |
|
cvc5
|
0
|
217
|
1513.12 |
1540.16 |
217 |
217 |
0 |
6 |
77 |
6 |
0 |
|
OpenSMT
|
0
|
215
|
2815.60 |
2842.32 |
215 |
215 |
0 |
8 |
77 |
8 |
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
|
65
|
742.10 |
750.38 |
65 |
0 |
65 |
0 |
235 |
0 |
0 |
|
cvc5
|
0
|
64
|
311.34 |
319.26 |
64 |
0 |
64 |
1 |
235 |
1 |
0 |
|
SMTInterpol
|
0
|
64
|
3831.93 |
3191.61 |
64 |
0 |
64 |
1 |
235 |
1 |
0 |
|
OpenSMT
|
0
|
63
|
1266.09 |
1274.01 |
63 |
0 |
63 |
2 |
235 |
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
|
275
|
171.43 |
205.68 |
275 |
211 |
64 |
0 |
25 |
0 |
0 |
|
cvc5
|
0
|
267
|
238.23 |
271.20 |
267 |
208 |
59 |
0 |
33 |
0 |
0 |
|
OpenSMT
|
0
|
265
|
405.16 |
437.67 |
265 |
205 |
60 |
0 |
35 |
0 |
0 |
|
SMTInterpol
|
0
|
263
|
948.60 |
427.05 |
263 |
208 |
55 |
0 |
37 |
0 |
0 |