QF_UFDTLIA (Unsat Core Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
SMTInterpol	27718	2293.01	2025.54	13	13	0	0
z3-BooledASS ^ne	27023 (base +0)	252.77	254.16	11	11	2	2
cvc5	13464	715.53	716.70	9	9	4	4
z3-BooledASS-base ⁿ	27023	251.52	252.91	11	11	2	2

(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
SMTInterpol	27718	2293.01	2025.54	13	13	0	0
z3-BooledASS ^ne	27023 (base +0)	252.77	254.16	11	11	2	2
cvc5	13464	715.53	716.70	9	9	4	4
z3-BooledASS-base ⁿ	27023	251.52	252.91	11	11	2	2

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
SMTInterpol	27718	2293.01	2025.54	13	13	0	0
z3-BooledASS ^ne	27023 (base +0)	252.77	254.16	11	11	2	2
cvc5	13464	715.53	716.70	9	9	4	4
z3-BooledASS-base ⁿ	27023	251.52	252.91	11	11	2	2

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
z3-BooledASS ^ne	23596 (base +0)	50.78	51.89	9	9	4
cvc5	5274	71.90	72.78	7	7	6
SMTInterpol	2662	82.69	32.94	5	5	8
z3-BooledASS-base ⁿ	23596	48.67	49.80	9	9	4

SMT-COMP 2026