QF_UFDTNIA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Z3-alpha2	61 (base +4)	4148.69	4121.69	61	47	14	19	19
Z3-alpha2-debug ⁿ	61	4280.34	4195.21	61	47	14	19	19
z3-BooledASS ^ne	57 (base -2)	3941.28	3948.54	57	43	14	23	23
cvc5-cvc5-xyz ^ne	39 (base +2)	3961.38	3966.56	39	28	11	41	41
cvc5	37	1943.26	1948.08	37	27	10	43	43
SMTInterpol	29	2752.22	2300.03	29	19	10	51	8
Xolver	0	0.00	0.00	0	0	0	80	80
z3-BooledASS-base ⁿ	59	4648.94	4656.69	59	44	15	21	21
Z3-alpha2-base ⁿ	57	2754.19	2761.54	57	42	15	23	23
cvc5-cvc5-xyz-base ⁿ	37	2240.46	2245.31	37	27	10	43	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-alpha2	61 (base +4)	4148.69	4121.69	61	47	14	19	19
Z3-alpha2-debug ⁿ	61	4280.34	4195.21	61	47	14	19	19
z3-BooledASS ^ne	57 (base -2)	3941.28	3948.54	57	43	14	23	23
cvc5-cvc5-xyz ^ne	39 (base +2)	3961.38	3966.56	39	28	11	41	41
cvc5	37	1943.26	1948.08	37	27	10	43	43
SMTInterpol	29	2752.22	2300.03	29	19	10	51	8
Xolver	0	0.00	0.00	0	0	0	80	80
z3-BooledASS-base ⁿ	59	4648.94	4656.69	59	44	15	21	21
Z3-alpha2-base ⁿ	57	2754.19	2761.54	57	42	15	23	23
cvc5-cvc5-xyz-base ⁿ	37	2240.46	2245.31	37	27	10	43	43

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Z3-alpha2	47 (base +5)	3773.05	3752.31	47	47	2	31	2
Z3-alpha2-debug ⁿ	47	3874.17	3808.65	47	47	2	31	2
z3-BooledASS ^ne	43 (base -1)	3182.20	3187.66	43	43	6	31	6
cvc5-cvc5-xyz ^ne	28 (base +1)	2449.29	2452.97	28	28	21	31	21
cvc5	27	728.94	732.33	27	27	22	31	22
SMTInterpol	19	1539.33	1263.39	19	19	30	31	4
Xolver	0	0.00	0.00	0	0	49	31	49
z3-BooledASS-base ⁿ	44	3120.47	3126.19	44	44	5	31	5
Z3-alpha2-base ⁿ	42	1014.59	1019.94	42	42	7	31	7
cvc5-cvc5-xyz-base ⁿ	27	871.69	875.12	27	27	22	31	22

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2 ^ne	14 (base -1)	375.65	369.37	14	14	4	62	4
Z3-alpha2-debug ⁿ	14	406.17	386.55	14	14	4	62	4
z3-BooledASS ^ne	14 (base -1)	759.08	760.88	14	14	4	62	4
cvc5-cvc5-xyz	11 (base +1)	1512.09	1513.59	11	11	7	62	7
SMTInterpol	10	1212.89	1036.65	10	10	8	62	0
cvc5	10	1214.31	1215.75	10	10	8	62	8
Xolver	0	0.00	0.00	0	0	18	62	18
z3-BooledASS-base ⁿ	15	1528.47	1530.49	15	15	3	62	3
Z3-alpha2-base ⁿ	15	1739.60	1741.60	15	15	3	62	3
cvc5-cvc5-xyz-base ⁿ	10	1368.78	1370.19	10	10	8	62	8

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-alpha2 ^ne	50 (base +2)	412.20	389.72	50	40	10	0	30
Z3-alpha2-debug ⁿ	49	490.71	422.02	49	39	10	0	31
z3-BooledASS ^ne	46 (base -1)	186.76	192.40	46	37	9	0	34
cvc5-cvc5-xyz ^ne	25 (base +4)	123.74	126.83	25	18	7	0	55
cvc5	23	117.41	120.28	23	17	6	0	57
SMTInterpol	16	263.31	115.69	16	10	6	22	42
Z3-alpha2-base ⁿ	48	228.43	234.44	48	37	11	0	32
z3-BooledASS-base ⁿ	47	194.72	200.59	47	38	9	0	33
cvc5-cvc5-xyz-base ⁿ	21	88.38	90.97	21	15	6	0	59

SMT-COMP 2026