QF_LIA (Model Validation Track)

Competition results for the QF_LIA logic in the Model Validation Track. Chart

Results were generated on 2026-07-25

Benchmarks: 1221
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	-	Yices2

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
OpenSMT	1164	53513.54	53663.97	1164	1164	57	57
Yices2	1142	13999.40	14142.79	1142	1142	79	79
SMTInterpol	1080	34809.10	28556.14	1081	1081	140	139
z3-BooledASS ^ne	1069 (base -28)	25720.42	25854.23	1069	1069	152	121
cvc5	921	37032.77	37150.90	921	921	300	300
z3-BooledASS-base ⁿ	1097	26652.38	26789.59	1097	1097	124	121

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
OpenSMT	1164	53513.54	53663.97	1164	1164	57	57
Yices2	1142	13999.40	14142.79	1142	1142	79	79
SMTInterpol	1081	36024.82	29739.62	1081	1081	140	139
z3-BooledASS ^ne	1069 (base -28)	25720.42	25854.23	1069	1069	152	121
cvc5	921	37032.77	37150.90	921	921	300	300
z3-BooledASS-base ⁿ	1097	26652.38	26789.59	1097	1097	124	121

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
OpenSMT	1164	53513.54	53663.97	1164	1164	57	57
Yices2	1142	13999.40	14142.79	1142	1142	79	79
SMTInterpol	1081	36024.82	29739.62	1081	1081	140	139
z3-BooledASS ^ne	1069 (base -28)	25720.42	25854.23	1069	1069	152	121
cvc5	921	37032.77	37150.90	921	921	300	300
z3-BooledASS-base ⁿ	1097	26652.38	26789.59	1097	1097	124	121

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
Yices2	1087	699.28	834.78	1087	1087	0	134
z3-BooledASS ^ne	976 (base -23)	777.23	897.30	976	976	26	219
OpenSMT	944	1406.18	1523.93	944	944	0	277
SMTInterpol	903	4159.66	2051.15	903	903	0	318
cvc5	817	703.13	804.53	817	817	0	404
z3-BooledASS-base ⁿ	999	996.80	1119.70	999	999	3	219

SMT-COMP 2026