QF_RDL (Single Query Track)

Competition results for the QF_RDL logic in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Yices2	216	4069.79	4096.87	216	107	109	31	31
cvc5	210	5384.59	5411.02	210	102	108	37	37
z3-BooledASS ^ne	208 (base +0)	5185.46	5211.59	208	100	108	39	39
cvc5-cvc5-xyz ^ne	206 (base -1)	8112.23	8138.29	206	100	106	41	41
Z3-GEX ^ne	205 (base -3)	6288.95	1700.01	209	101	108	38	38
OpenSMT	199	14777.18	14803.24	199	103	96	48	48
OpenSMT-SMTS-seq ^ne	195 (base -3)	14222.45	13948.34	196	102	94	51	51
SMTInterpol	175	7387.81	5197.43	175	97	78	72	68
Z3-GEX-base ⁿ	208	5051.28	5078.07	208	100	108	39	39
z3-BooledASS-base ⁿ	208	5246.88	5273.05	208	100	108	39	39
cvc5-cvc5-xyz-base ⁿ	207	9211.71	9238.29	207	101	106	40	40
OpenSMT-SMTS-seq-base ⁿ	198	14103.43	14129.33	198	103	95	49	49

(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	Solved UNSAT	Unsolved	Timeout
Yices2	216	4069.79	4096.87	216	107	109	31	31
cvc5	210	5384.59	5411.02	210	102	108	37	37
Z3-GEX ^ne	209 (base +1)	16613.47	4299.73	209	101	108	38	38
z3-BooledASS ^ne	208 (base +0)	5185.46	5211.59	208	100	108	39	39
cvc5-cvc5-xyz ^ne	206 (base -1)	8112.23	8138.29	206	100	106	41	41
OpenSMT	199	14777.18	14803.24	199	103	96	48	48
OpenSMT-SMTS-seq ^ne	196 (base -2)	15432.93	15136.72	196	102	94	51	51
SMTInterpol	175	7387.81	5197.43	175	97	78	72	68
Z3-GEX-base ⁿ	208	5051.28	5078.07	208	100	108	39	39
z3-BooledASS-base ⁿ	208	5246.88	5273.05	208	100	108	39	39
cvc5-cvc5-xyz-base ⁿ	207	9211.71	9238.29	207	101	106	40	40
OpenSMT-SMTS-seq-base ⁿ	198	14103.43	14129.33	198	103	95	49	49

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Yices2	107	2351.78	2365.15	107	107	0	140	0
OpenSMT	103	6309.00	6322.35	103	103	4	140	4
cvc5	102	1832.32	1845.06	102	102	5	140	5
OpenSMT-SMTS-seq ^ne	102 (base -1)	7916.44	7762.34	102	102	5	140	5
Z3-GEX	101 (base +1)	8360.71	2163.13	101	101	6	140	6
z3-BooledASS ^ne	100 (base +0)	3360.31	3372.97	100	100	7	140	7
cvc5-cvc5-xyz ^ne	100 (base -1)	3767.75	3780.39	100	100	7	140	7
SMTInterpol	97	3123.13	2370.78	97	97	10	140	10
OpenSMT-SMTS-seq-base ⁿ	103	6566.79	6579.97	103	103	4	140	4
cvc5-cvc5-xyz-base ⁿ	101	4913.43	4926.46	101	101	6	140	6
Z3-GEX-base ⁿ	100	3264.66	3277.64	100	100	7	140	7
z3-BooledASS-base ⁿ	100	3410.53	3423.23	100	100	7	140	7

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Yices2	109	1718.01	1731.72	109	109	0	138	0
z3-BooledASS ^ne	108 (base +0)	1825.14	1838.62	108	108	1	138	1
Z3-GEX ^ne	108 (base +0)	8252.76	2136.60	108	108	1	138	1
cvc5	108	3552.27	3565.96	108	108	1	138	1
cvc5-cvc5-xyz ^ne	106 (base +0)	4344.48	4357.90	106	106	3	138	3
OpenSMT	96	8468.18	8480.88	96	96	13	138	13
OpenSMT-SMTS-seq ^ne	94 (base -1)	7516.49	7374.38	94	94	15	138	15
SMTInterpol	78	4264.68	2826.65	78	78	31	138	27
Z3-GEX-base ⁿ	108	1786.62	1800.43	108	108	1	138	1
z3-BooledASS-base ⁿ	108	1836.34	1849.82	108	108	1	138	1
cvc5-cvc5-xyz-base ⁿ	106	4298.28	4311.83	106	106	3	138	3
OpenSMT-SMTS-seq-base ⁿ	95	7536.64	7549.37	95	95	14	138	14

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
Yices2	199	344.32	368.93	199	99	100	48
Z3-GEX ^ne	191 (base +5)	1740.60	523.28	191	94	97	56
z3-BooledASS ^ne	186 (base +0)	453.79	476.68	186	91	95	61
cvc5	175	601.34	622.95	175	92	83	72
OpenSMT	151	389.97	408.61	151	83	68	96
cvc5-cvc5-xyz ^ne	151 (base +1)	611.62	630.22	151	76	75	96
OpenSMT-SMTS-seq ^ne	149 (base -2)	388.99	397.76	149	81	68	98
SMTInterpol	135	1449.08	666.62	135	75	60	112
Z3-GEX-base ⁿ	186	442.97	466.31	186	91	95	61
z3-BooledASS-base ⁿ	186	456.72	479.65	186	91	95	61
OpenSMT-SMTS-seq-base ⁿ	151	404.26	422.99	151	83	68	96
cvc5-cvc5-xyz-base ⁿ	150	584.09	602.74	150	76	74	97

SMT-COMP 2026