UFDTLIA (Unsat Core Track)

Competition results for the UFDTLIA logic in the Unsat Core Track. Chart

Results were generated on 2026-07-25

Benchmarks: 532
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	z3-BooledASS

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	316959 (base +1673)	269.47	324.87	450	450	82	32
cvc5	316852	11822.83	11881.32	466	466	66	43
SMTInterpol	54875	2662.91	1863.42	123	123	409	311
z3-BooledASS-base ⁿ	315286	146.58	201.41	447	447	85	27

(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	Timeout
z3-BooledASS ^ne	316959 (base +1673)	269.47	324.87	450	450	82	32
cvc5	316852	11822.83	11881.32	466	466	66	43
SMTInterpol	55248	4253.10	2980.78	123	123	409	311
z3-BooledASS-base ⁿ	315286	146.58	201.41	447	447	85	27

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	316959 (base +1673)	269.47	324.87	450	450	82	32
cvc5	316852	11822.83	11881.32	466	466	66	43
SMTInterpol	55248	4253.10	2980.78	123	123	409	311
z3-BooledASS-base ⁿ	315286	146.58	201.41	447	447	85	27

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained
z3-BooledASS	316527 (base +1241)	142.18	197.44	449	449	37	46
cvc5	301999	567.52	621.88	441	441	17	74
SMTInterpol	50759	635.50	247.87	108	108	0	424
z3-BooledASS-base ⁿ	315286	146.58	201.41	447	447	42	43

SMT-COMP 2026