UFBV (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 144
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	z3-BooledASS	Bitwuzla	Bitwuzla

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	103 (base +0)	3637.12	3650.19	103	35	68	41	40
cvc5-cvc5-xyz ^ne	98 (base +1)	7361.34	7374.12	98	21	77	46	18
cvc5	97	6674.96	6687.49	97	20	77	47	17
Bitwuzla-fixed ⁿ	96	1032.25	1044.10	96	17	79	48	48
Bitwuzla	95	771.39	783.32	95	17	78	49	49
bitwuzla-dandelion ⁿ	93 (base -2)	1085.34	1097.14	93	19	74	51	50
UltimateEliminator+MathSAT	6	42.91	16.77	6	0	6	138	28
SMTInterpol	0	0.00	0.00	0	0	0	144	89
z3-BooledASS-base ⁿ	103	4709.46	4722.60	103	35	68	41	40
cvc5-cvc5-xyz-base ⁿ	97	6654.53	6667.21	97	20	77	47	17
bitwuzla-dandelion-base ⁿ	95	532.32	544.24	95	19	76	49	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	103 (base +0)	3637.12	3650.19	103	35	68	41	40
cvc5-cvc5-xyz ^ne	98 (base +1)	7361.34	7374.12	98	21	77	46	18
cvc5	97	6674.96	6687.49	97	20	77	47	17
Bitwuzla-fixed ⁿ	96	1032.25	1044.10	96	17	79	48	48
Bitwuzla	95	771.39	783.32	95	17	78	49	49
bitwuzla-dandelion ⁿ	93 (base -2)	1085.34	1097.14	93	19	74	51	50
UltimateEliminator+MathSAT	6	42.91	16.77	6	0	6	138	28
SMTInterpol	0	0.00	0.00	0	0	0	144	89
z3-BooledASS-base ⁿ	103	4709.46	4722.60	103	35	68	41	40
cvc5-cvc5-xyz-base ⁿ	97	6654.53	6667.21	97	20	77	47	17
bitwuzla-dandelion-base ⁿ	95	532.32	544.24	95	19	76	49	49

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS	35 (base +0)	399.35	403.69	35	35	2	107	1
cvc5-cvc5-xyz ^ne	21 (base +1)	3733.13	3736.11	21	21	16	107	1
cvc5	20	3044.25	3046.98	20	20	17	107	1
bitwuzla-dandelion ⁿ	19 (base +0)	79.89	82.27	19	19	18	107	18
Bitwuzla	17	65.18	67.33	17	17	20	107	20
Bitwuzla-fixed ⁿ	17	65.76	67.82	17	17	20	107	20
SMTInterpol	0	0.00	0.00	0	0	37	107	25
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	37	107	18
z3-BooledASS-base ⁿ	35	1193.92	1198.42	35	35	2	107	1
cvc5-cvc5-xyz-base ⁿ	20	3043.00	3045.83	20	20	17	107	1
bitwuzla-dandelion-base ⁿ	19	66.58	68.96	19	19	18	107	18

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla-fixed ⁿ	79	966.49	976.28	79	79	8	57	8
Bitwuzla	78	706.21	715.99	78	78	9	57	9
cvc5-cvc5-xyz ^ne	77 (base +0)	3628.22	3638.01	77	77	10	57	4
cvc5	77	3630.71	3640.51	77	77	10	57	3
bitwuzla-dandelion ⁿ	74 (base -2)	1005.45	1014.87	74	74	13	57	12
z3-BooledASS ^ne	68 (base +0)	3237.77	3246.50	68	68	19	57	19
UltimateEliminator+MathSAT	6	42.91	16.77	6	6	81	57	6
SMTInterpol	0	0.00	0.00	0	0	87	57	46
cvc5-cvc5-xyz-base ⁿ	77	3611.53	3621.37	77	77	10	57	3
bitwuzla-dandelion-base ⁿ	76	465.74	475.28	76	76	11	57	11
z3-BooledASS-base ⁿ	68	3515.55	3524.18	68	68	19	57	19

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
bitwuzla-dandelion ⁿ	92 (base -2)	221.36	232.91	92	19	73	1	51
z3-BooledASS ^ne	85 (base +5)	158.66	169.02	85	33	52	0	59
Bitwuzla-fixed ⁿ	85	193.22	203.59	85	16	69	0	59
Bitwuzla	85	194.12	204.74	85	16	69	0	59
cvc5	61	182.65	190.18	61	1	60	0	83
cvc5-cvc5-xyz ^ne	61 (base +0)	185.17	192.63	61	1	60	0	83
UltimateEliminator+MathSAT	6	42.91	16.77	6	0	6	107	31
SMTInterpol	0	0.00	0.00	0	0	0	33	111
bitwuzla-dandelion-base ⁿ	94	201.39	213.18	94	19	75	0	50
z3-BooledASS-base ⁿ	80	71.11	80.81	80	29	51	0	64
cvc5-cvc5-xyz-base ⁿ	61	183.17	190.76	61	1	60	0	83

SMT-COMP 2026