QF_UFIDL (Model Validation Track)

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

Results were generated on 2026-07-25

Benchmarks: 206
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	-	SMTInterpol

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
OpenSMT	199	6193.10	6218.71	199	199	7	7
z3-BooledASS ^ne	179 (base +0)	1768.86	1790.57	179	179	27	27
SMTInterpol	177	4592.57	3489.91	178	178	28	28
cvc5	175	23386.63	23410.81	175	175	31	31
Yices2	145	13919.08	13938.50	145	145	61	61
z3-BooledASS-base ⁿ	179	1764.07	1786.11	179	179	27	27

(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	199	6193.10	6218.71	199	199	7	7
z3-BooledASS ^ne	179 (base +0)	1768.86	1790.57	179	179	27	27
SMTInterpol	178	5839.55	4647.38	178	178	28	28
cvc5	175	23386.63	23410.81	175	175	31	31
Yices2	145	13919.08	13938.50	145	145	61	61
z3-BooledASS-base ⁿ	179	1764.07	1786.11	179	179	27	27

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
OpenSMT	199	6193.10	6218.71	199	199	7	7
z3-BooledASS ^ne	179 (base +0)	1768.86	1790.57	179	179	27	27
SMTInterpol	178	5839.55	4647.38	178	178	28	28
cvc5	175	23386.63	23410.81	175	175	31	31
Yices2	145	13919.08	13938.50	145	145	61	61
z3-BooledASS-base ⁿ	179	1764.07	1786.11	179	179	27	27

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Abstained
z3-BooledASS ^ne	172 (base +0)	210.81	231.52	172	172	34
SMTInterpol	164	1407.20	601.20	164	164	42
OpenSMT	161	495.53	515.75	161	161	45
Yices2	108	46.73	60.21	108	108	98
cvc5	107	77.42	90.64	107	107	99
z3-BooledASS-base ⁿ	172	210.04	231.13	172	172	34

SMT-COMP 2026