Equality (Single Query Track)

Competition results for the Equality division in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Logics:

UF : 971 benchmarks
UFDT : 713 benchmarks

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	Abstained	Timeout
cvc5-cvc5-xyz ^ne	653 (base +0)	106629.43	106718.02	653	185	468	1031	0	1031
cvc5	653	107709.06	107798.26	653	185	468	1031	0	1031
z3-BooledASS ^ne	266 (base +1)	4113.41	4146.48	266	29	237	1418	0	1267
Yices2	116	6909.49	6924.55	116	13	103	855	713	854
SMTInterpol	90	6206.37	5411.48	91	4	87	1593	0	1500
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	971	713	0
cvc5-cvc5-xyz-base ⁿ	653	107697.08	107786.50	653	185	468	1031	0	1031
z3-BooledASS-base ⁿ	265	2694.95	2727.67	265	29	236	1419	0	1148

(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	Abstained	Timeout
cvc5-cvc5-xyz ^ne	653 (base +0)	106629.43	106718.02	653	185	468	1031	0	1031
cvc5	653	107709.06	107798.26	653	185	468	1031	0	1031
z3-BooledASS ^ne	266 (base +1)	4113.41	4146.48	266	29	237	1418	0	1267
Yices2	116	6909.49	6924.55	116	13	103	855	713	854
SMTInterpol	91	7440.98	6450.46	91	4	87	1593	0	1500
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	971	713	0
cvc5-cvc5-xyz-base ⁿ	653	107697.08	107786.50	653	185	468	1031	0	1031
z3-BooledASS-base ⁿ	265	2694.95	2727.67	265	29	236	1419	0	1148

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	185 (base +0)	93938.29	93968.68	185	185	8	1491	8
cvc5	185	93956.85	93987.46	185	185	8	1491	8
z3-BooledASS ^ne	29 (base +0)	70.90	74.50	29	29	164	1491	135
Yices2	13	666.40	668.08	13	13	119	1552	119
SMTInterpol	4	37.83	24.21	4	4	189	1491	155
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	132	1552	0
cvc5-cvc5-xyz-base ⁿ	185	93940.67	93971.36	185	185	8	1491	8
z3-BooledASS-base ⁿ	29	74.22	77.81	29	29	164	1491	121

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	468 (base +0)	12691.13	12749.34	468	468	13	1203	13
cvc5	468	13752.22	13810.80	468	468	13	1203	13
z3-BooledASS ^ne	237 (base +1)	4042.51	4071.98	237	237	244	1203	228
Yices2	103	6243.09	6256.47	103	103	179	1402	179
SMTInterpol	87	7403.16	6426.24	87	87	394	1203	384
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	282	1402	0
cvc5-cvc5-xyz-base ⁿ	468	13756.41	13815.14	468	468	13	1203	13
z3-BooledASS-base ⁿ	236	2620.73	2649.86	236	236	245	1203	206

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
cvc5-cvc5-xyz ^ne	381 (base +3)	371.42	418.04	381	6	375	0	1303
cvc5	378	348.00	394.41	378	6	372	0	1306
z3-BooledASS ^ne	249 (base -1)	172.86	203.43	249	27	222	6	1429
Yices2	94	122.58	134.12	94	12	82	1	1589
SMTInterpol	68	517.74	242.33	68	4	64	32	1584
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	971	713
cvc5-cvc5-xyz-base ⁿ	378	351.82	398.19	378	6	372	0	1306
z3-BooledASS-base ⁿ	250	177.37	208.01	250	27	223	5	1429

SMT-COMP 2026