UFDTNIRA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 806
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
cvc5	745	537.55	631.31	745	0	745	61	16
cvc5-cvc5-xyz ^ne	745 (base +0)	546.51	638.37	745	0	745	61	16
z3-BooledASS ^ne	718 (base -2)	132.97	221.29	718	10	708	88	88
SMTInterpol	555	7483.83	5571.01	555	0	555	251	153
cvc5-cvc5-xyz-base ⁿ	745	541.95	633.76	745	0	745	61	16
z3-BooledASS-base ⁿ	720	453.90	542.27	720	10	710	86	86

(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
cvc5	745	537.55	631.31	745	0	745	61	16
cvc5-cvc5-xyz ^ne	745 (base +0)	546.51	638.37	745	0	745	61	16
z3-BooledASS ^ne	718 (base -2)	132.97	221.29	718	10	708	88	88
SMTInterpol	555	7483.83	5571.01	555	0	555	251	153
cvc5-cvc5-xyz-base ⁿ	745	541.95	633.76	745	0	745	61	16
z3-BooledASS-base ⁿ	720	453.90	542.27	720	10	710	86	86

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	10 (base +0)	1.72	2.95	10	10	0	796	0
SMTInterpol	0	0.00	0.00	0	0	10	796	0
cvc5	0	0.00	0.00	0	0	10	796	2
cvc5-cvc5-xyz ^ne	0 (base +0)	0.00	0.00	0	0	10	796	2
z3-BooledASS-base ⁿ	10	1.69	2.91	10	10	0	796	0
cvc5-cvc5-xyz-base ⁿ	0	0.00	0.00	0	0	10	796	2

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	745	537.55	631.31	745	745	2	59	2
cvc5-cvc5-xyz ^ne	745 (base +0)	546.51	638.37	745	745	2	59	2
z3-BooledASS ^ne	708 (base -2)	131.24	218.34	708	708	39	59	39
SMTInterpol	555	7483.83	5571.01	555	555	192	59	105
cvc5-cvc5-xyz-base ⁿ	745	541.95	633.76	745	745	2	59	2
z3-BooledASS-base ⁿ	710	452.21	539.36	710	710	37	59	37

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
cvc5	744	155.16	248.75	744	0	744	45	17
cvc5-cvc5-xyz ^ne	744 (base +0)	158.64	250.35	744	0	744	45	17
z3-BooledASS ^ne	718 (base -1)	132.97	221.29	718	10	708	0	88
SMTInterpol	539	1692.91	706.18	539	0	539	32	235
cvc5-cvc5-xyz-base ⁿ	744	158.59	250.25	744	0	744	45	17
z3-BooledASS-base ⁿ	719	135.34	223.57	719	10	709	0	87

SMT-COMP 2026