QF_UFIDL (Single Query Track)
Competition results for the QF_UFIDL
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) |
|
OpenSMT
|
OpenSMT
|
OpenSMT
|
OpenSMT
|
OpenSMT
|
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
|
273
|
20638.16 |
20675.06 |
273 |
100 |
173 |
27 |
0 |
27 |
0 |
|
cvc5
|
0
|
237
|
27640.78 |
27674.46 |
237 |
87 |
150 |
63 |
0 |
63 |
0 |
|
Yices2
|
0
|
227
|
15279.35 |
15309.39 |
227 |
70 |
157 |
73 |
0 |
73 |
0 |
|
SMTInterpol
|
0
|
205
|
5793.79 |
3783.10 |
205 |
91 |
114 |
95 |
0 |
81 |
0 |
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
|
273
|
20638.16 |
20675.06 |
273 |
100 |
173 |
27 |
0 |
27 |
0 |
|
cvc5
|
0
|
237
|
27640.78 |
27674.46 |
237 |
87 |
150 |
63 |
0 |
63 |
0 |
|
Yices2
|
0
|
227
|
15279.35 |
15309.39 |
227 |
70 |
157 |
73 |
0 |
73 |
0 |
|
SMTInterpol
|
0
|
205
|
5793.79 |
3783.10 |
205 |
91 |
114 |
95 |
0 |
81 |
0 |
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
|
100
|
3479.67 |
3492.61 |
100 |
100 |
0 |
4 |
196 |
4 |
0 |
|
SMTInterpol
|
0
|
91
|
3079.54 |
2445.14 |
91 |
91 |
0 |
13 |
196 |
13 |
0 |
|
cvc5
|
0
|
87
|
10294.54 |
10306.96 |
87 |
87 |
0 |
17 |
196 |
17 |
0 |
|
Yices2
|
0
|
70
|
6918.15 |
6927.81 |
70 |
70 |
0 |
34 |
196 |
34 |
0 |
UNSAT Performance Performance
| Solver |
Error Score |
Correct Score |
CPU Time Score |
Wall Time Score |
Solved |
Solved SAT |
Solved UNSAT |
Unsolved |
Abstained |
Timeout |
Memout |
|
OpenSMT
|
0
|
173
|
17158.49 |
17182.45 |
173 |
0 |
173 |
23 |
104 |
23 |
0 |
|
Yices2
|
0
|
157
|
8361.20 |
8381.58 |
157 |
0 |
157 |
39 |
104 |
39 |
0 |
|
cvc5
|
0
|
150
|
17346.23 |
17367.50 |
150 |
0 |
150 |
46 |
104 |
46 |
0 |
|
SMTInterpol
|
0
|
114
|
2714.25 |
1337.96 |
114 |
0 |
114 |
82 |
104 |
68 |
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 |
|
OpenSMT
|
0
|
194
|
642.96 |
667.08 |
194 |
82 |
112 |
0 |
106 |
0 |
0 |
|
SMTInterpol
|
0
|
188
|
2154.22 |
926.26 |
188 |
84 |
104 |
0 |
112 |
0 |
0 |
|
Yices2
|
0
|
186
|
142.78 |
165.66 |
186 |
53 |
133 |
0 |
114 |
0 |
0 |
|
cvc5
|
0
|
146
|
363.77 |
381.69 |
146 |
52 |
94 |
0 |
154 |
0 |
0 |