QF_UFDTLIRA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 9
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	cvc5

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT
z3-BooledASS ^ne	9 (base +0)	1.45	2.53	9	5	4
cvc5	9	1.43	2.54	9	5	4
cvc5-cvc5-xyz ^ne	9 (base +0)	1.50	2.61	9	5	4
SMTInterpol	9	4.62	4.30	9	5	4
cvc5-cvc5-xyz-base ⁿ	9	1.51	2.65	9	5	4
z3-BooledASS-base ⁿ	9	1.60	2.68	9	5	4

(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
z3-BooledASS ^ne	9 (base +0)	1.45	2.53	9	5	4
cvc5	9	1.43	2.54	9	5	4
cvc5-cvc5-xyz ^ne	9 (base +0)	1.50	2.61	9	5	4
SMTInterpol	9	4.62	4.30	9	5	4
cvc5-cvc5-xyz-base ⁿ	9	1.51	2.65	9	5	4
z3-BooledASS-base ⁿ	9	1.60	2.68	9	5	4

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Abstained
cvc5	5	0.79	1.40	5	5	4
cvc5-cvc5-xyz ^ne	5 (base +0)	0.82	1.44	5	5	4
z3-BooledASS ^ne	5 (base +0)	0.83	1.44	5	5	4
SMTInterpol	5	2.43	2.33	5	5	4
z3-BooledASS-base ⁿ	5	0.84	1.43	5	5	4
cvc5-cvc5-xyz-base ⁿ	5	0.84	1.47	5	5	4

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
z3-BooledASS	4 (base +0)	0.62	1.09	4	4	5
cvc5	4	0.64	1.14	4	4	5
cvc5-cvc5-xyz ^ne	4 (base +0)	0.68	1.17	4	4	5
SMTInterpol	4	2.18	1.97	4	4	5
cvc5-cvc5-xyz-base ⁿ	4	0.67	1.18	4	4	5
z3-BooledASS-base ⁿ	4	0.76	1.25	4	4	5

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT
z3-BooledASS ^ne	9 (base +0)	1.45	2.53	9	5	4
cvc5	9	1.43	2.54	9	5	4
cvc5-cvc5-xyz ^ne	9 (base +0)	1.50	2.61	9	5	4
SMTInterpol	9	4.62	4.30	9	5	4
cvc5-cvc5-xyz-base ⁿ	9	1.51	2.65	9	5	4
z3-BooledASS-base ⁿ	9	1.60	2.68	9	5	4

SMT-COMP 2026