QF_UFNIA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 339
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Yices2	Yices2	Yices2	Z3-alpha2	Yices2

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Yices2	286	6719.49	6755.76	286	235	51	53	53
Z3-alpha2 ^ne	272 (base +7)	9716.55	9591.61	272	202	70	67	67
Z3-alpha2-debug ⁿ	272	10280.63	9897.04	272	202	70	67	67
z3-BooledASS ^ne	265 (base +3)	5567.11	5599.99	265	197	68	74	74
cvc5	225	3315.20	3343.30	225	166	59	114	114
cvc5-cvc5-xyz ^ne	225 (base +0)	4436.25	4464.17	225	166	59	114	114
Xolver	150	257.72	276.45	150	128	22	189	185
SMTInterpol	119	13413.06	12180.74	119	86	33	220	44
Z3-alpha2-base ⁿ	265	6187.28	6220.69	265	199	66	74	74
z3-BooledASS-base ⁿ	262	5691.47	5724.75	262	194	68	77	77
cvc5-cvc5-xyz-base ⁿ	225	4375.03	4403.33	225	166	59	114	114

(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
Yices2	286	6719.49	6755.76	286	235	51	53	53
Z3-alpha2 ^ne	272 (base +7)	9716.55	9591.61	272	202	70	67	67
Z3-alpha2-debug ⁿ	272	10280.63	9897.04	272	202	70	67	67
z3-BooledASS ^ne	265 (base +3)	5567.11	5599.99	265	197	68	74	74
cvc5	225	3315.20	3343.30	225	166	59	114	114
cvc5-cvc5-xyz ^ne	225 (base +0)	4436.25	4464.17	225	166	59	114	114
Xolver	150	257.72	276.45	150	128	22	189	185
SMTInterpol	119	13413.06	12180.74	119	86	33	220	44
Z3-alpha2-base ⁿ	265	6187.28	6220.69	265	199	66	74	74
z3-BooledASS-base ⁿ	262	5691.47	5724.75	262	194	68	77	77
cvc5-cvc5-xyz-base ⁿ	225	4375.03	4403.33	225	166	59	114	114

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Yices2	235	6288.89	6318.80	235	235	6	98	6
Z3-alpha2 ^ne	202 (base +3)	6694.28	6601.35	202	202	39	98	39
Z3-alpha2-debug ⁿ	202	7114.87	6830.08	202	202	39	98	39
z3-BooledASS ^ne	197 (base +3)	4180.79	4205.30	197	197	44	98	44
cvc5	166	2976.36	2997.10	166	166	75	98	75
cvc5-cvc5-xyz ^ne	166 (base +0)	3998.40	4019.08	166	166	75	98	75
Xolver	128	177.09	193.07	128	128	113	98	109
SMTInterpol	86	11131.28	10137.56	86	86	155	98	23
Z3-alpha2-base ⁿ	199	4687.38	4712.43	199	199	42	98	42
z3-BooledASS-base ⁿ	194	3960.82	3985.57	194	194	47	98	47
cvc5-cvc5-xyz-base ⁿ	166	3940.51	3961.40	166	166	75	98	75

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2	70 (base +4)	3022.27	2990.26	70	70	5	264	5
Z3-alpha2-debug ⁿ	70	3165.76	3066.96	70	70	5	264	5
z3-BooledASS ^ne	68 (base +0)	1386.32	1394.69	68	68	7	264	7
cvc5	59	338.85	346.20	59	59	16	264	16
cvc5-cvc5-xyz ^ne	59 (base +0)	437.84	445.09	59	59	16	264	16
Yices2	51	430.61	436.96	51	51	24	264	24
SMTInterpol	33	2281.77	2043.17	33	33	42	264	6
Xolver	22	80.62	83.38	22	22	53	264	53
z3-BooledASS-base ⁿ	68	1730.66	1739.18	68	68	7	264	7
Z3-alpha2-base ⁿ	66	1499.90	1508.26	66	66	9	264	9
cvc5-cvc5-xyz-base ⁿ	59	434.52	441.93	59	59	16	264	16

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Yices2	249	355.90	386.81	249	200	49	0	90
Z3-alpha2 ^ne	243 (base +1)	1186.00	1074.60	243	181	62	0	96
Z3-alpha2-debug ⁿ	243	1703.76	1361.01	243	181	62	0	96
z3-BooledASS ^ne	242 (base +2)	415.37	445.02	242	180	62	0	97
cvc5	205	204.47	229.78	205	150	55	0	134
cvc5-cvc5-xyz	201 (base -1)	153.17	177.76	201	147	54	0	138
Xolver	150	257.72	276.45	150	128	22	4	185
SMTInterpol	76	258.83	127.82	76	49	27	159	104
Z3-alpha2-base ⁿ	242	417.06	447.07	242	181	61	0	97
z3-BooledASS-base ⁿ	240	391.56	421.64	240	178	62	0	99
cvc5-cvc5-xyz-base ⁿ	202	177.49	202.45	202	148	54	0	137

SMT-COMP 2026