QF_AUFLIA (Single Query Track)
Competition results for the QF_AUFLIA
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 534
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Winners
| Sequential Performance |
Parallel Performance |
SAT Performance (parallel) |
UNSAT Performance (parallel) |
24 seconds Performance (parallel) |
|
Yices2
|
Yices2
|
Yices2
|
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 |
|
Yices2
|
0
|
534
|
89.93 |
156.16 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
|
cvc5
|
0
|
534
|
203.26 |
269.63 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
|
SMTInterpol
|
0
|
534
|
1257.85 |
637.91 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
|
OpenSMT
|
0
|
534
|
624.46 |
690.54 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
Parallel Performance Performance
| Solver |
Error Score |
Correct Score |
CPU Time Score |
Wall Time Score |
Solved |
Solved SAT |
Solved UNSAT |
Unsolved |
Abstained |
Timeout |
Memout |
|
Yices2
|
0
|
534
|
89.93 |
156.16 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
|
cvc5
|
0
|
534
|
203.26 |
269.63 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
|
SMTInterpol
|
0
|
534
|
1257.85 |
637.91 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
|
OpenSMT
|
0
|
534
|
624.46 |
690.54 |
534 |
274 |
260 |
0 |
0 |
0 |
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
|
274
|
43.54 |
77.66 |
274 |
274 |
0 |
0 |
260 |
0 |
0 |
|
OpenSMT
|
0
|
274
|
102.13 |
136.05 |
274 |
274 |
0 |
0 |
260 |
0 |
0 |
|
cvc5
|
0
|
274
|
109.67 |
143.69 |
274 |
274 |
0 |
0 |
260 |
0 |
0 |
|
SMTInterpol
|
0
|
274
|
265.85 |
166.39 |
274 |
274 |
0 |
0 |
260 |
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 |
|
Yices2
|
0
|
260
|
46.38 |
78.51 |
260 |
0 |
260 |
0 |
274 |
0 |
0 |
|
cvc5
|
0
|
260
|
93.58 |
125.95 |
260 |
0 |
260 |
0 |
274 |
0 |
0 |
|
SMTInterpol
|
0
|
260
|
992.01 |
471.52 |
260 |
0 |
260 |
0 |
274 |
0 |
0 |
|
OpenSMT
|
0
|
260
|
522.33 |
554.49 |
260 |
0 |
260 |
0 |
274 |
0 |
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
|
534
|
89.93 |
156.16 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
|
cvc5
|
0
|
534
|
203.26 |
269.63 |
534 |
274 |
260 |
0 |
0 |
0 |
0 |
|
OpenSMT
|
0
|
533
|
211.70 |
277.61 |
533 |
274 |
259 |
0 |
1 |
0 |
0 |
|
SMTInterpol
|
0
|
532
|
912.32 |
474.77 |
532 |
274 |
258 |
0 |
2 |
0 |
0 |