QF_UFLRA (Model Validation Track)

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

Results were generated on 2026-07-25

Benchmarks: 385
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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Yices2	384	364.26	412.16	384	384	1	1
SMTInterpol	384	2812.32	1551.03	384	384	1	1
cvc5	383	256.39	303.58	383	383	2	2
OpenSMT	381	2244.50	2292.08	381	381	4	4
z3-BooledASS ^ne	253 (base +0)	48.86	79.82	253	253	132	12
z3-BooledASS-base ⁿ	253	49.14	80.34	253	253	132	12

(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
Yices2	384	364.26	412.16	384	384	1	1
SMTInterpol	384	2812.32	1551.03	384	384	1	1
cvc5	383	256.39	303.58	383	383	2	2
OpenSMT	381	2244.50	2292.08	381	381	4	4
z3-BooledASS ^ne	253 (base +0)	48.86	79.82	253	253	132	12
z3-BooledASS-base ⁿ	253	49.14	80.34	253	253	132	12

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Yices2	384	364.26	412.16	384	384	1	1
SMTInterpol	384	2812.32	1551.03	384	384	1	1
cvc5	383	256.39	303.58	383	383	2	2
OpenSMT	381	2244.50	2292.08	381	381	4	4
z3-BooledASS ^ne	253 (base +0)	48.86	79.82	253	253	132	12
z3-BooledASS-base ⁿ	253	49.14	80.34	253	253	132	12

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
Yices2	383	78.66	126.43	383	383	0	2
SMTInterpol	381	1179.35	506.37	381	381	0	4
cvc5	380	121.01	167.81	380	380	0	5
OpenSMT	373	270.75	317.10	373	373	0	12
z3-BooledASS ^ne	253 (base +0)	48.86	79.82	253	253	107	25
z3-BooledASS-base ⁿ	253	49.14	80.34	253	253	107	25

SMT-COMP 2026