QF_UF (Single Query Track)
Competition results for the QF_UF
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 3521
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
|
3521
|
1599.77 |
2035.93 |
3521 |
1473 |
2048 |
0 |
0 |
0 |
0 |
|
OpenSMT
|
0
|
3520
|
7474.78 |
7912.01 |
3520 |
1473 |
2047 |
1 |
0 |
1 |
0 |
|
cvc5
|
0
|
3519
|
5055.83 |
5489.34 |
3519 |
1473 |
2046 |
2 |
0 |
2 |
0 |
|
SMTInterpol
|
0
|
3443
|
24749.86 |
11485.66 |
3443 |
1473 |
1970 |
78 |
0 |
24 |
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
|
3521
|
1599.77 |
2035.93 |
3521 |
1473 |
2048 |
0 |
0 |
0 |
0 |
|
OpenSMT
|
0
|
3520
|
7474.78 |
7912.01 |
3520 |
1473 |
2047 |
1 |
0 |
1 |
0 |
|
cvc5
|
0
|
3519
|
5055.83 |
5489.34 |
3519 |
1473 |
2046 |
2 |
0 |
2 |
0 |
|
SMTInterpol
|
0
|
3443
|
24749.86 |
11485.66 |
3443 |
1473 |
1970 |
78 |
0 |
24 |
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
|
1473
|
246.82 |
429.58 |
1473 |
1473 |
0 |
0 |
2048 |
0 |
0 |
|
OpenSMT
|
0
|
1473
|
384.08 |
567.08 |
1473 |
1473 |
0 |
0 |
2048 |
0 |
0 |
|
cvc5
|
0
|
1473
|
475.70 |
657.38 |
1473 |
1473 |
0 |
0 |
2048 |
0 |
0 |
|
SMTInterpol
|
0
|
1473
|
3689.56 |
1742.13 |
1473 |
1473 |
0 |
0 |
2048 |
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
|
2048
|
1352.94 |
1606.35 |
2048 |
0 |
2048 |
0 |
1473 |
0 |
0 |
|
OpenSMT
|
0
|
2047
|
7090.70 |
7344.94 |
2047 |
0 |
2047 |
1 |
1473 |
1 |
0 |
|
cvc5
|
0
|
2046
|
4580.13 |
4831.97 |
2046 |
0 |
2046 |
2 |
1473 |
2 |
0 |
|
SMTInterpol
|
0
|
1970
|
21060.30 |
9743.53 |
1970 |
0 |
1970 |
78 |
1473 |
24 |
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
|
3518
|
687.03 |
1122.70 |
3518 |
1473 |
2045 |
0 |
3 |
0 |
0 |
|
OpenSMT
|
0
|
3494
|
2019.55 |
2452.78 |
3494 |
1473 |
2021 |
0 |
27 |
0 |
0 |
|
cvc5
|
0
|
3487
|
1834.66 |
2263.82 |
3487 |
1473 |
2014 |
0 |
34 |
0 |
0 |
|
SMTInterpol
|
0
|
3408
|
18844.45 |
8529.55 |
3408 |
1472 |
1936 |
0 |
113 |
0 |
0 |