UFNIRA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 258
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	105 (base +0)	35.46	48.39	105	16	89	153	138
cvc5	72	850.47	859.59	72	0	72	186	49
cvc5-cvc5-xyz ^ne	72 (base +0)	1141.76	1150.73	72	0	72	186	49
SMTInterpol	12	7.90	6.44	12	0	12	246	122
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	258	9
z3-BooledASS-base ⁿ	105	33.67	46.60	105	16	89	153	121
cvc5-cvc5-xyz-base ⁿ	72	1140.74	1149.80	72	0	72	186	49

(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	105 (base +0)	35.46	48.39	105	16	89	153	138
cvc5	72	850.47	859.59	72	0	72	186	49
cvc5-cvc5-xyz ^ne	72 (base +0)	1141.76	1150.73	72	0	72	186	49
SMTInterpol	12	7.90	6.44	12	0	12	246	122
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	258	9
z3-BooledASS-base ⁿ	105	33.67	46.60	105	16	89	153	121
cvc5-cvc5-xyz-base ⁿ	72	1140.74	1149.80	72	0	72	186	49

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	16 (base +0)	2.76	4.75	16	16	63	179	56
SMTInterpol	0	0.00	0.00	0	0	79	179	53
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	79	179	2
cvc5	0	0.00	0.00	0	0	79	179	3
cvc5-cvc5-xyz ^ne	0 (base +0)	0.00	0.00	0	0	79	179	3
z3-BooledASS-base ⁿ	16	2.74	4.71	16	16	63	179	53
cvc5-cvc5-xyz-base ⁿ	0	0.00	0.00	0	0	79	179	3

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	89 (base +0)	32.71	43.64	89	89	90	79	82
cvc5	72	850.47	859.59	72	72	107	79	46
cvc5-cvc5-xyz ^ne	72 (base +0)	1141.76	1150.73	72	72	107	79	46
SMTInterpol	12	7.90	6.44	12	12	167	79	69
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	179	79	7
z3-BooledASS-base ⁿ	89	30.93	41.89	89	89	90	79	68
cvc5-cvc5-xyz-base ⁿ	72	1140.74	1149.80	72	72	107	79	46

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	105 (base +0)	35.46	48.39	105	16	89	8	145
cvc5	70	45.02	53.78	70	0	70	137	51
cvc5-cvc5-xyz ^ne	70 (base +0)	65.37	73.99	70	0	70	137	51
SMTInterpol	12	7.90	6.44	12	0	12	124	122
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	0	249	9
z3-BooledASS-base ⁿ	105	33.67	46.60	105	16	89	8	145
cvc5-cvc5-xyz-base ⁿ	70	65.54	74.27	70	0	70	137	51

SMT-COMP 2026