QF_UFDT (Single Query Track)

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

Results were generated on 2026-07-25

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
cvc5-cvc5-xyz ^ne	173 (base +0)	51644.97	51670.85	173	83	90	27	27
cvc5	169	50530.81	50556.41	169	83	86	31	31
Z3-alpha2	120 (base +17)	28929.76	28881.46	120	28	92	80	80
Z3-alpha2-debug ⁿ	120	29153.28	28991.74	120	28	92	80	80
z3-BooledASS ^ne	102 (base +0)	27196.54	27211.45	102	9	93	98	98
SMTInterpol	30	7225.54	5747.48	31	24	7	169	149
cvc5-cvc5-xyz-base ⁿ	173	51217.47	51243.70	173	83	90	27	27
Z3-alpha2-base ⁿ	103	28554.34	28569.70	103	10	93	97	97
z3-BooledASS-base ⁿ	102	27565.81	27584.08	102	9	93	98	98

(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-cvc5-xyz ^ne	173 (base +0)	51644.97	51670.85	173	83	90	27	27
cvc5	169	50530.81	50556.41	169	83	86	31	31
Z3-alpha2	120 (base +17)	28929.76	28881.46	120	28	92	80	80
Z3-alpha2-debug ⁿ	120	29153.28	28991.74	120	28	92	80	80
z3-BooledASS ^ne	102 (base +0)	27196.54	27211.45	102	9	93	98	98
SMTInterpol	31	8484.99	6228.44	31	24	7	169	149
cvc5-cvc5-xyz-base ⁿ	173	51217.47	51243.70	173	83	90	27	27
Z3-alpha2-base ⁿ	103	28554.34	28569.70	103	10	93	97	97
z3-BooledASS-base ⁿ	102	27565.81	27584.08	102	9	93	98	98

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	83 (base +0)	8744.42	8755.51	83	83	17	100	17
cvc5	83	8820.64	8831.94	83	83	17	100	17
Z3-alpha2	28 (base +18)	4898.55	4886.88	28	28	72	100	72
Z3-alpha2-debug ⁿ	28	4947.74	4909.76	28	28	72	100	72
SMTInterpol	24	4863.94	4517.42	24	24	76	100	76
z3-BooledASS ^ne	9 (base +0)	4845.85	4847.41	9	9	91	100	91
cvc5-cvc5-xyz-base ⁿ	83	8836.15	8847.48	83	83	17	100	17
Z3-alpha2-base ⁿ	10	5971.61	5973.34	10	10	90	100	90
z3-BooledASS-base ⁿ	9	4880.54	4882.37	9	9	91	100	91

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	93 (base +0)	22350.69	22364.04	93	93	7	100	7
Z3-alpha2 ^ne	92 (base -1)	24031.22	23994.58	92	92	8	100	8
Z3-alpha2-debug ⁿ	92	24205.53	24081.98	92	92	8	100	8
cvc5-cvc5-xyz ^ne	90 (base +0)	42900.55	42915.33	90	90	10	100	10
cvc5	86	41710.18	41724.48	86	86	14	100	14
SMTInterpol	7	3621.05	1711.02	7	7	93	100	73
Z3-alpha2-base ⁿ	93	22582.73	22596.36	93	93	7	100	7
z3-BooledASS-base ⁿ	93	22685.27	22701.70	93	93	7	100	7
cvc5-cvc5-xyz-base ⁿ	90	42381.32	42396.22	90	90	10	100	10

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
cvc5-cvc5-xyz ^ne	20 (base +0)	276.00	278.51	20	18	2	180
cvc5	19	255.83	258.22	19	18	1	181
Z3-alpha2 ^ne	14 (base +10)	216.94	210.97	14	9	5	186
Z3-alpha2-debug ⁿ	14	246.93	227.45	14	9	5	186
SMTInterpol	7	138.66	74.36	7	7	0	193
z3-BooledASS ^ne	5 (base +0)	103.70	104.32	5	0	5	195
cvc5-cvc5-xyz-base ⁿ	20	277.67	280.18	20	18	2	180
z3-BooledASS-base ⁿ	5	104.62	105.55	5	0	5	195
Z3-alpha2-base ⁿ	4	80.50	81.00	4	0	4	196

SMT-COMP 2026