QF_UFBV (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Bitwuzla	Bitwuzla	Bitwuzla	Bitwuzla	Bitwuzla

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
bitwuzla-dandelion ⁿ	513 (base +9)	17378.13	17444.51	513	213	300	39	39
Bitwuzla	505	16653.03	16718.95	505	213	292	47	47
Yices2	459	42691.29	42752.05	459	206	253	93	93
cvc5-cvc5-xyz ^ne	440 (base +0)	118929.88	118999.70	440	179	261	112	112
cvc5	440	119110.60	119181.24	440	179	261	112	112
SMTInterpol	340	22985.32	17421.75	340	88	252	212	108
z3-BooledASS ^ne	273 (base -93)	22079.92	22115.64	273	129	144	279	184
bitwuzla-dandelion-base ⁿ	504	16042.08	16107.20	504	211	293	48	48
cvc5-cvc5-xyz-base ⁿ	440	119481.53	119552.97	440	179	261	112	112
z3-BooledASS-base ⁿ	366	38458.17	38506.90	366	170	196	186	185

(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
bitwuzla-dandelion ⁿ	513 (base +9)	17378.13	17444.51	513	213	300	39	39
Bitwuzla	505	16653.03	16718.95	505	213	292	47	47
Yices2	459	42691.29	42752.05	459	206	253	93	93
cvc5-cvc5-xyz ^ne	440 (base +0)	118929.88	118999.70	440	179	261	112	112
cvc5	440	119110.60	119181.24	440	179	261	112	112
SMTInterpol	340	22985.32	17421.75	340	88	252	212	108
z3-BooledASS ^ne	273 (base -93)	22079.92	22115.64	273	129	144	279	184
bitwuzla-dandelion-base ⁿ	504	16042.08	16107.20	504	211	293	48	48
cvc5-cvc5-xyz-base ⁿ	440	119481.53	119552.97	440	179	261	112	112
z3-BooledASS-base ⁿ	366	38458.17	38506.90	366	170	196	186	185

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla	213	8732.03	8760.15	213	213	0	339	0
bitwuzla-dandelion ⁿ	213 (base +2)	9440.63	9468.58	213	213	0	339	0
Yices2	206	13700.68	13727.51	206	206	7	339	7
cvc5-cvc5-xyz ^ne	179 (base +0)	23143.22	23168.07	179	179	34	339	34
cvc5	179	23193.53	23218.57	179	179	34	339	34
z3-BooledASS ^ne	129 (base -41)	6764.96	6781.47	129	129	84	339	43
SMTInterpol	88	14007.35	12078.05	88	88	125	339	44
bitwuzla-dandelion-base ⁿ	211	8371.10	8398.69	211	211	2	339	2
cvc5-cvc5-xyz-base ⁿ	179	23159.20	23184.18	179	179	34	339	34
z3-BooledASS-base ⁿ	170	9727.02	9748.87	170	170	43	339	42

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
bitwuzla-dandelion ⁿ	300 (base +7)	7937.50	7975.93	300	300	12	240	12
Bitwuzla	292	7921.00	7958.81	292	292	20	240	20
cvc5-cvc5-xyz ^ne	261 (base +0)	95786.67	95831.63	261	261	51	240	51
cvc5	261	95917.06	95962.67	261	261	51	240	51
Yices2	253	28990.61	29024.54	253	253	59	240	59
SMTInterpol	252	8977.97	5343.70	252	252	60	240	54
z3-BooledASS ^ne	144 (base -52)	15314.96	15334.17	144	144	168	240	114
bitwuzla-dandelion-base ⁿ	293	7670.98	7708.51	293	293	19	240	19
cvc5-cvc5-xyz-base ⁿ	261	96322.33	96368.79	261	261	51	240	51
z3-BooledASS-base ⁿ	196	28731.15	28758.03	196	196	116	240	116

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
bitwuzla-dandelion ⁿ	368 (base +1)	3452.58	3499.10	368	127	241	0	184
Bitwuzla	338	2656.02	2698.64	338	127	211	0	214
Yices2	317	2340.90	2380.36	317	145	172	0	235
SMTInterpol	261	6035.31	2560.42	261	43	218	48	243
z3-BooledASS ^ne	193 (base -30)	949.27	973.08	193	106	87	34	325
cvc5	101	649.30	661.84	101	84	17	0	451
cvc5-cvc5-xyz ^ne	100 (base +0)	620.97	633.29	100	83	17	0	452
bitwuzla-dandelion-base ⁿ	367	3126.71	3172.90	367	130	237	0	185
z3-BooledASS-base ⁿ	223	1177.53	1204.92	223	131	92	0	329
cvc5-cvc5-xyz-base ⁿ	100	620.00	632.39	100	83	17	0	452

SMT-COMP 2026