QF_IDL (Model Validation Track)

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

Results were generated on 2026-07-25

Benchmarks: 548
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
z3-BooledASS ^ne	494 (base -1)	24209.35	24271.75	494	494	54	51
Yices2	483	11930.41	11991.30	483	483	65	62
OpenSMT	444	28861.39	28919.12	444	444	104	103
cvc5	425	37999.61	38056.03	425	425	123	122
SMTInterpol	328	23210.51	19807.48	328	328	220	219
z3-BooledASS-base ⁿ	495	22826.37	22888.67	495	495	53	52

(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
z3-BooledASS ^ne	494 (base -1)	24209.35	24271.75	494	494	54	51
Yices2	483	11930.41	11991.30	483	483	65	62
OpenSMT	444	28861.39	28919.12	444	444	104	103
cvc5	425	37999.61	38056.03	425	425	123	122
SMTInterpol	328	23210.51	19807.48	328	328	220	219
z3-BooledASS-base ⁿ	495	22826.37	22888.67	495	495	53	52

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
z3-BooledASS ^ne	494 (base -1)	24209.35	24271.75	494	494	54	51
Yices2	483	11930.41	11991.30	483	483	65	62
OpenSMT	444	28861.39	28919.12	444	444	104	103
cvc5	425	37999.61	38056.03	425	425	123	122
SMTInterpol	328	23210.51	19807.48	328	328	220	219
z3-BooledASS-base ⁿ	495	22826.37	22888.67	495	495	53	52

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
Yices2	435	704.81	758.90	435	435	2	111
z3-BooledASS ^ne	404 (base -1)	1007.26	1056.97	404	404	2	142
OpenSMT	296	1183.33	1220.10	296	296	0	252
cvc5	273	1062.08	1095.69	273	273	0	275
SMTInterpol	234	2731.55	1309.18	234	234	0	314
z3-BooledASS-base ⁿ	405	995.86	1045.70	405	405	1	142

SMT-COMP 2026