UF (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 971
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5	cvc5	cvc5	cvc5	cvc5

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
cvc5-cvc5-xyz ^ne	400 (base +0)	70869.78	70924.37	400	125	275	571	571
cvc5	400	70881.63	70936.56	400	125	275	571	571
z3-BooledASS ^ne	159 (base +1)	2933.79	2953.61	159	21	138	812	748
Yices2	116	6909.49	6924.55	116	13	103	855	854
SMTInterpol	62	5393.52	4797.61	63	3	60	908	866
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	971	0
cvc5-cvc5-xyz-base ⁿ	400	70873.11	70928.17	400	125	275	571	571
z3-BooledASS-base ⁿ	158	1361.58	1381.13	158	21	137	813	653

(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
cvc5-cvc5-xyz ^ne	400 (base +0)	70869.78	70924.37	400	125	275	571	571
cvc5	400	70881.63	70936.56	400	125	275	571	571
z3-BooledASS ^ne	159 (base +1)	2933.79	2953.61	159	21	138	812	748
Yices2	116	6909.49	6924.55	116	13	103	855	854
SMTInterpol	63	6628.13	5836.59	63	3	60	908	866
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	971	0
cvc5-cvc5-xyz-base ⁿ	400	70873.11	70928.17	400	125	275	571	571
z3-BooledASS-base ⁿ	158	1361.58	1381.13	158	21	137	813	653

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	125 (base +0)	65136.10	65156.58	125	125	7	839	7
cvc5	125	65149.07	65169.91	125	125	7	839	7
z3-BooledASS ^ne	21 (base +0)	69.11	71.69	21	21	111	839	100
Yices2	13	666.40	668.08	13	13	119	839	119
SMTInterpol	3	36.95	23.63	3	3	129	839	113
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	132	839	0
cvc5-cvc5-xyz-base ⁿ	125	65136.76	65157.53	125	125	7	839	7
z3-BooledASS-base ⁿ	21	72.59	75.18	21	21	111	839	86

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	275	5732.56	5766.65	275	275	7	689	7
cvc5-cvc5-xyz ^ne	275 (base +0)	5733.68	5767.79	275	275	7	689	7
z3-BooledASS ^ne	138 (base +1)	2864.68	2881.91	138	138	144	689	137
Yices2	103	6243.09	6256.47	103	103	179	689	179
SMTInterpol	60	6591.18	5812.97	60	60	222	689	216
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	282	689	0
cvc5-cvc5-xyz-base ⁿ	275	5736.35	5770.64	275	275	7	689	7
z3-BooledASS-base ⁿ	137	1288.99	1305.95	137	137	145	689	121

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
cvc5	230	225.58	253.76	230	5	225	0	741
cvc5-cvc5-xyz ^ne	230 (base +0)	225.99	254.12	230	5	225	0	741
z3-BooledASS ^ne	145 (base -1)	134.76	152.59	145	19	126	0	826
Yices2	94	122.58	134.12	94	12	82	1	876
SMTInterpol	45	335.24	160.53	45	3	42	5	921
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	971	0
cvc5-cvc5-xyz-base ⁿ	230	227.69	255.91	230	5	225	0	741
z3-BooledASS-base ⁿ	146	139.21	157.17	146	19	127	0	825

SMT-COMP 2026