UFLRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	4 (base -1)	5.22	5.69	4	2	2	3	3
cvc5-cvc5-xyz ^ne	2 (base +0)	0.31	0.56	2	0	2	5	4
cvc5	2	0.34	0.60	2	0	2	5	4
SMTInterpol	2	1.02	0.95	2	0	2	5	4
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	7	0
z3-BooledASS-base ⁿ	5	408.78	409.43	5	3	2	2	2
cvc5-cvc5-xyz-base ⁿ	2	0.31	0.56	2	0	2	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	Unsolved	Timeout
z3-BooledASS ^ne	4 (base -1)	5.22	5.69	4	2	2	3	3
cvc5-cvc5-xyz ^ne	2 (base +0)	0.31	0.56	2	0	2	5	4
cvc5	2	0.34	0.60	2	0	2	5	4
SMTInterpol	2	1.02	0.95	2	0	2	5	4
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	7	0
z3-BooledASS-base ⁿ	5	408.78	409.43	5	3	2	2	2
cvc5-cvc5-xyz-base ⁿ	2	0.31	0.56	2	0	2	5	4

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	2 (base -1)	4.92	5.16	2	2	3	2	3
SMTInterpol	0	0.00	0.00	0	0	5	2	4
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	5	2	0
cvc5	0	0.00	0.00	0	0	5	2	4
cvc5-cvc5-xyz ^ne	0 (base +0)	0.00	0.00	0	0	5	2	4
z3-BooledASS-base ⁿ	3	408.45	408.85	3	3	2	2	2
cvc5-cvc5-xyz-base ⁿ	0	0.00	0.00	0	0	5	2	4

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	2 (base +0)	0.30	0.53	2	2	0	5
cvc5-cvc5-xyz ^ne	2 (base +0)	0.31	0.56	2	2	0	5
cvc5	2	0.34	0.60	2	2	0	5
SMTInterpol	2	1.02	0.95	2	2	0	5
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	2	5
cvc5-cvc5-xyz-base ⁿ	2	0.31	0.56	2	2	0	5
z3-BooledASS-base ⁿ	2	0.33	0.58	2	2	0	5

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	4 (base +1)	5.22	5.69	4	2	2	0	3
cvc5-cvc5-xyz ^ne	2 (base +0)	0.31	0.56	2	0	2	0	5
cvc5	2	0.34	0.60	2	0	2	0	5
SMTInterpol	2	1.02	0.95	2	0	2	1	4
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	7	0
z3-BooledASS-base ⁿ	3	2.06	2.44	3	1	2	0	4
cvc5-cvc5-xyz-base ⁿ	2	0.31	0.56	2	0	2	0	5

SMT-COMP 2026