QF_UFLRA (Single Query Track)
Competition results for the QF_UFLRA
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 541
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
|
539
|
832.19 |
899.15 |
539 |
331 |
208 |
2 |
0 |
2 |
0 |
|
cvc5
|
0
|
538
|
776.05 |
842.32 |
538 |
330 |
208 |
3 |
0 |
3 |
0 |
|
SMTInterpol
|
0
|
537
|
3147.77 |
1277.42 |
537 |
330 |
207 |
4 |
0 |
4 |
0 |
|
OpenSMT
|
0
|
535
|
544.67 |
610.77 |
535 |
327 |
208 |
6 |
0 |
6 |
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
|
539
|
832.19 |
899.15 |
539 |
331 |
208 |
2 |
0 |
2 |
0 |
|
cvc5
|
0
|
538
|
776.05 |
842.32 |
538 |
330 |
208 |
3 |
0 |
3 |
0 |
|
SMTInterpol
|
0
|
537
|
3147.77 |
1277.42 |
537 |
330 |
207 |
4 |
0 |
4 |
0 |
|
OpenSMT
|
0
|
535
|
544.67 |
610.77 |
535 |
327 |
208 |
6 |
0 |
6 |
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
|
331
|
795.47 |
836.64 |
331 |
331 |
0 |
1 |
209 |
1 |
0 |
|
cvc5
|
0
|
330
|
676.02 |
716.69 |
330 |
330 |
0 |
2 |
209 |
2 |
0 |
|
SMTInterpol
|
0
|
330
|
2133.91 |
847.11 |
330 |
330 |
0 |
2 |
209 |
2 |
0 |
|
OpenSMT
|
0
|
327
|
482.90 |
523.32 |
327 |
327 |
0 |
5 |
209 |
5 |
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
|
208
|
36.71 |
62.51 |
208 |
0 |
208 |
0 |
333 |
0 |
0 |
|
OpenSMT
|
0
|
208
|
61.76 |
87.45 |
208 |
0 |
208 |
0 |
333 |
0 |
0 |
|
cvc5
|
0
|
208
|
100.04 |
125.63 |
208 |
0 |
208 |
0 |
333 |
0 |
0 |
|
SMTInterpol
|
0
|
207
|
1013.86 |
430.31 |
207 |
0 |
207 |
1 |
333 |
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 |
|
Yices2
|
0
|
538
|
106.30 |
173.07 |
538 |
330 |
208 |
0 |
3 |
0 |
0 |
|
cvc5
|
0
|
533
|
170.83 |
236.42 |
533 |
326 |
207 |
0 |
8 |
0 |
0 |
|
SMTInterpol
|
0
|
532
|
1993.53 |
807.46 |
532 |
326 |
206 |
0 |
9 |
0 |
0 |
|
OpenSMT
|
0
|
530
|
306.74 |
372.17 |
530 |
322 |
208 |
0 |
11 |
0 |
0 |