Equality (Unsat Core Track)

Competition results for the Equality division in the Unsat Core Track. Chart

Results were generated on 2026-07-25

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

Logics:

UF : 740 benchmarks
UFDT : 596 benchmarks

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	420491	10771.82	10936.73	1326	1326	10	0	10
z3-BooledASS ^ne	349080 (base -17)	2031.56	2167.17	1106	1106	230	0	209
SMTInterpol	222385	32823.22	28809.95	726	726	610	0	591
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	740	596	0
z3-BooledASS-base ⁿ	349097	2427.89	2563.43	1106	1106	230	0	182

(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 UNSAT	Unsolved	Abstained	Timeout
cvc5	420491	10771.82	10936.73	1326	1326	10	0	10
z3-BooledASS ^ne	349080 (base -17)	2031.56	2167.17	1106	1106	230	0	209
SMTInterpol	222395	34151.08	29846.35	726	726	610	0	591
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	740	596	0
z3-BooledASS-base ⁿ	349097	2427.89	2563.43	1106	1106	230	0	182

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	420491	10771.82	10936.73	1326	1326	10	0	10
z3-BooledASS ^ne	349080 (base -17)	2031.56	2167.17	1106	1106	230	0	209
SMTInterpol	222395	34151.08	29846.35	726	726	610	0	591
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	740	596	0
z3-BooledASS-base ⁿ	349097	2427.89	2563.43	1106	1106	230	0	182

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained
cvc5	397537	531.10	685.39	1248	1248	0	88
z3-BooledASS ^ne	344525 (base +791)	465.45	599.15	1092	1092	3	241
SMTInterpol	198734	3301.00	1546.12	632	632	3	701
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	740	596
z3-BooledASS-base ⁿ	343734	398.18	531.17	1087	1087	3	246

SMT-COMP 2026