UFDTLIRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	949 (base -1)	743.47	860.31	949	173	776	121	119
cvc5	936	492.58	607.89	936	156	780	134	43
cvc5-cvc5-xyz ^ne	936 (base +0)	501.80	617.22	936	156	780	134	43
SMTInterpol	874	4257.41	2991.90	874	133	741	196	38
z3-BooledASS-base ⁿ	950	739.79	856.47	950	174	776	120	119
cvc5-cvc5-xyz-base ⁿ	936	503.76	619.33	936	156	780	134	43

(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	Timeout
z3-BooledASS ^ne	949 (base -1)	743.47	860.31	949	173	776	121	119
cvc5	936	492.58	607.89	936	156	780	134	43
cvc5-cvc5-xyz ^ne	936 (base +0)	501.80	617.22	936	156	780	134	43
SMTInterpol	874	4257.41	2991.90	874	133	741	196	38
z3-BooledASS-base ⁿ	950	739.79	856.47	950	174	776	120	119
cvc5-cvc5-xyz-base ⁿ	936	503.76	619.33	936	156	780	134	43

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	173 (base -1)	603.12	624.45	173	173	1	896	0
cvc5	156	349.58	368.31	156	156	18	896	5
cvc5-cvc5-xyz ^ne	156 (base +0)	358.09	376.78	156	156	18	896	5
SMTInterpol	133	87.52	69.65	133	133	41	896	4
z3-BooledASS-base ⁿ	174	598.50	619.99	174	174	0	896	0
cvc5-cvc5-xyz-base ⁿ	156	358.28	376.94	156	156	18	896	5

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	780	143.00	239.58	780	780	0	290	0
cvc5-cvc5-xyz ^ne	780 (base +0)	143.71	240.44	780	780	0	290	0
z3-BooledASS ^ne	776 (base +0)	140.35	235.86	776	776	4	290	3
SMTInterpol	741	4169.88	2922.25	741	741	39	290	25
cvc5-cvc5-xyz-base ⁿ	780	145.48	242.39	780	780	0	290	0
z3-BooledASS-base ⁿ	776	141.28	236.48	776	776	4	290	3

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	945 (base -1)	204.02	320.29	945	169	776	2	123
cvc5	933	188.27	303.20	933	153	780	20	117
cvc5-cvc5-xyz ^ne	933 (base +0)	191.87	306.91	933	153	780	21	116
SMTInterpol	859	1596.33	828.45	859	133	726	145	66
z3-BooledASS-base ⁿ	946	205.93	322.07	946	170	776	1	123
cvc5-cvc5-xyz-base ⁿ	933	193.55	308.72	933	153	780	20	117

SMT-COMP 2026