QF_Equality_LinearArith (Single Query Track)
Competition results for the QF_Equality_LinearArith
division
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 1936
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Logics:
Winners
| Sequential Performance |
Parallel Performance |
SAT Performance (parallel) |
UNSAT Performance (parallel) |
24 seconds Performance (parallel) |
|
SMTInterpol
|
SMTInterpol
|
SMTInterpol
|
OpenSMT
|
SMTInterpol
|
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
|
1798
|
29410.55 |
21874.66 |
1798 |
1064 |
734 |
138 |
0 |
117 |
0 |
|
cvc5
|
0
|
1795
|
40758.29 |
40986.45 |
1795 |
1031 |
764 |
141 |
0 |
141 |
0 |
|
OpenSMT
|
0
|
1778
|
30357.19 |
30581.04 |
1778 |
1002 |
776 |
73 |
85 |
73 |
0 |
|
Yices2
|
0
|
1744
|
19780.59 |
19999.59 |
1744 |
982 |
762 |
107 |
85 |
107 |
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
|
1798
|
29410.55 |
21874.66 |
1798 |
1064 |
734 |
138 |
0 |
117 |
0 |
|
cvc5
|
0
|
1795
|
40758.29 |
40986.45 |
1795 |
1031 |
764 |
141 |
0 |
141 |
0 |
|
OpenSMT
|
0
|
1778
|
30357.19 |
30581.04 |
1778 |
1002 |
776 |
73 |
85 |
73 |
0 |
|
Yices2
|
0
|
1744
|
19780.59 |
19999.59 |
1744 |
982 |
762 |
107 |
85 |
107 |
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
|
1064
|
17863.19 |
13942.77 |
1064 |
1064 |
0 |
19 |
853 |
16 |
0 |
|
cvc5
|
0
|
1031
|
20983.36 |
21113.94 |
1031 |
1031 |
0 |
52 |
853 |
52 |
0 |
|
OpenSMT
|
0
|
1002
|
11021.72 |
11146.88 |
1002 |
1002 |
0 |
31 |
903 |
31 |
0 |
|
Yices2
|
0
|
982
|
10579.41 |
10702.92 |
982 |
982 |
0 |
51 |
903 |
51 |
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
|
776
|
19335.47 |
19434.16 |
776 |
0 |
776 |
25 |
1135 |
25 |
0 |
|
cvc5
|
0
|
764
|
19774.93 |
19872.52 |
764 |
0 |
764 |
54 |
1118 |
54 |
0 |
|
Yices2
|
0
|
762
|
9201.17 |
9296.68 |
762 |
0 |
762 |
39 |
1135 |
39 |
0 |
|
SMTInterpol
|
0
|
734
|
11547.37 |
7931.89 |
734 |
0 |
734 |
84 |
1118 |
70 |
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 |
|
SMTInterpol
|
0
|
1709
|
7246.87 |
3178.66 |
1709 |
1007 |
702 |
4 |
223 |
0 |
0 |
|
Yices2
|
0
|
1693
|
592.95 |
802.92 |
1693 |
956 |
737 |
0 |
243 |
0 |
0 |
|
cvc5
|
0
|
1645
|
1437.68 |
1640.89 |
1645 |
952 |
693 |
0 |
291 |
0 |
0 |
|
OpenSMT
|
0
|
1645
|
1806.62 |
2009.77 |
1645 |
937 |
708 |
0 |
291 |
0 |
0 |