QF_RDL (Model Validation Track)

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

Results were generated on 2026-07-25

Benchmarks: 109
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	109	520.99	534.54	109	109	0	0
OpenSMT	107	6306.95	6320.68	107	107	2	2
cvc5	106	1888.69	1902.00	106	106	3	3
z3-BooledASS ^ne	104 (base +0)	3368.56	3381.72	104	104	5	5
SMTInterpol	101	3113.23	2356.36	101	101	8	8
z3-BooledASS-base ⁿ	104	3398.56	3411.73	104	104	5	5

(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	109	520.99	534.54	109	109	0	0
OpenSMT	107	6306.95	6320.68	107	107	2	2
cvc5	106	1888.69	1902.00	106	106	3	3
z3-BooledASS ^ne	104 (base +0)	3368.56	3381.72	104	104	5	5
SMTInterpol	101	3113.23	2356.36	101	101	8	8
z3-BooledASS-base ⁿ	104	3398.56	3411.73	104	104	5	5

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Yices2	109	520.99	534.54	109	109	0	0
OpenSMT	107	6306.95	6320.68	107	107	2	2
cvc5	106	1888.69	1902.00	106	106	3	3
z3-BooledASS ^ne	104 (base +0)	3368.56	3381.72	104	104	5	5
SMTInterpol	101	3113.23	2356.36	101	101	8	8
z3-BooledASS-base ⁿ	104	3398.56	3411.73	104	104	5	5

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Abstained
Yices2	103	97.61	110.39	103	103	6
z3-BooledASS ^ne	95 (base +0)	221.18	232.89	95	95	14
cvc5	94	297.70	309.34	94	94	15
OpenSMT	87	194.84	205.65	87	87	22
SMTInterpol	79	698.16	318.56	79	79	30
z3-BooledASS-base ⁿ	95	222.66	234.44	95	95	14

SMT-COMP 2026