BVFP (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 208
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	cvc5	Bitwuzla

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Bitwuzla-fixed ⁿ	203	54.96	79.89	203	191	12	5	5
Bitwuzla	203	54.92	80.06	203	191	12	5	5
cvc5	199	1319.84	1344.67	199	185	14	9	9
cvc5-cvc5-xyz ^ne	199 (base +0)	1324.78	1349.44	199	185	14	9	9
UltimateEliminator+MathSAT	37	363.53	260.28	37	35	2	171	1
colibri2	24	5.04	8.00	24	24	0	184	4
bitwuzla-dandelion ⁿ	0 (base -192)	0.00	0.00	0	0	0	208	0
z3-BooledASS ^ne	0 (base -180)	0.00	0.00	0	0	0	208	0
cvc5-cvc5-xyz-base ⁿ	199	1324.92	1349.67	199	185	14	9	9
bitwuzla-dandelion-base ⁿ	192	78.09	101.96	192	180	12	16	16
z3-BooledASS-base ⁿ	180	1672.29	1694.59	180	167	13	28	23

(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-fixed ⁿ	203	54.96	79.89	203	191	12	5	5
Bitwuzla	203	54.92	80.06	203	191	12	5	5
cvc5	199	1319.84	1344.67	199	185	14	9	9
cvc5-cvc5-xyz ^ne	199 (base +0)	1324.78	1349.44	199	185	14	9	9
UltimateEliminator+MathSAT	37	363.53	260.28	37	35	2	171	1
colibri2	24	5.04	8.00	24	24	0	184	4
bitwuzla-dandelion ⁿ	0 (base -192)	0.00	0.00	0	0	0	208	0
z3-BooledASS ^ne	0 (base -180)	0.00	0.00	0	0	0	208	0
cvc5-cvc5-xyz-base ⁿ	199	1324.92	1349.67	199	185	14	9	9
bitwuzla-dandelion-base ⁿ	192	78.09	101.96	192	180	12	16	16
z3-BooledASS-base ⁿ	180	1672.29	1694.59	180	167	13	28	23

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla	191	33.32	56.96	191	191	2	15	2
Bitwuzla-fixed ⁿ	191	33.56	57.00	191	191	2	15	2
cvc5	185	48.53	71.44	185	185	8	15	8
cvc5-cvc5-xyz ^ne	185 (base +0)	52.69	75.48	185	185	8	15	8
UltimateEliminator+MathSAT	35	313.99	230.97	35	35	158	15	0
colibri2	24	5.04	8.00	24	24	169	15	2
bitwuzla-dandelion ⁿ	0 (base -180)	0.00	0.00	0	0	193	15	0
z3-BooledASS ^ne	0 (base -167)	0.00	0.00	0	0	193	15	0
cvc5-cvc5-xyz-base ⁿ	185	53.43	76.25	185	185	8	15	8
bitwuzla-dandelion-base ⁿ	180	58.53	80.92	180	180	13	15	13
z3-BooledASS-base ⁿ	167	1429.17	1449.84	167	167	26	15	21

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	14	1271.31	1273.23	14	14	0	194	0
cvc5-cvc5-xyz ^ne	14 (base +0)	1272.09	1273.96	14	14	0	194	0
Bitwuzla-fixed ⁿ	12	21.40	22.89	12	12	2	194	2
Bitwuzla	12	21.59	23.09	12	12	2	194	2
UltimateEliminator+MathSAT	2	49.54	29.31	2	2	12	194	0
bitwuzla-dandelion ⁿ	0 (base -12)	0.00	0.00	0	0	14	194	0
colibri2	0	0.00	0.00	0	0	14	194	2
z3-BooledASS ^ne	0 (base -13)	0.00	0.00	0	0	14	194	0
cvc5-cvc5-xyz-base ⁿ	14	1271.49	1273.41	14	14	0	194	0
z3-BooledASS-base ⁿ	13	243.13	244.75	13	13	1	194	1
bitwuzla-dandelion-base ⁿ	12	19.56	21.05	12	12	2	194	2

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla-fixed ⁿ	203	54.96	79.89	203	191	12	0	5
Bitwuzla	203	54.92	80.06	203	191	12	0	5
cvc5	196	96.27	120.53	196	185	11	0	12
cvc5-cvc5-xyz ^ne	196 (base +0)	101.45	125.62	196	185	11	0	12
UltimateEliminator+MathSAT	34	257.94	162.85	34	32	2	168	6
colibri2	24	5.04	8.00	24	24	0	179	5
bitwuzla-dandelion ⁿ	0 (base -191)	0.00	0.00	0	0	0	208	0
z3-BooledASS ^ne	0 (base -173)	0.00	0.00	0	0	0	208	0
cvc5-cvc5-xyz-base ⁿ	196	101.90	126.12	196	185	11	0	12
bitwuzla-dandelion-base ⁿ	191	50.67	74.42	191	179	12	0	17
z3-BooledASS-base ⁿ	173	156.56	177.82	173	162	11	5	30

SMT-COMP 2026