QF_BV (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Bitwuzla-MachBV	0	2495 (base +17)	18732.06	19045.00	2495	1225	1270	45	45
Bitwuzla	0	2475	19066.80	19376.69	2475	1213	1262	65	65
bitwuzla-dandelion ⁿ	0	2472 (base -7)	181812.38	182137.12	2472	1221	1251	68	68
Bitwuzla-SPFD ^ne	0	2457 (base -21)	67200.71	67508.98	2457	1211	1246	83	83
bv_decide-nokernel	0	2404	128731.41	129084.44	2404	1180	1224	136	134
bv_decide	0	2401	157573.75	157937.31	2401	1179	1222	139	137
cvc5-cvc5-xyz ^ne	0	2375 (base +1)	77836.34	78137.09	2375	1187	1188	165	165
cvc5	0	2375	77951.89	78253.72	2375	1187	1188	165	165
NeuroSym	0	2358	7780.05	7513.73	2358	1162	1196	182	1
Z3-GEX	0	2229 (base +145)	110525.65	30303.90	2294	1119	1175	246	246
Z3-alpha2	0	2131 (base +48)	93661.23	93568.24	2131	1128	1003	409	409
Z3-alpha2-debug ⁿ	0	2130	99868.38	97735.79	2130	1127	1003	410	410
SMTInterpol	0	1007	126277.47	96935.40	1009	160	849	1531	1300
Roole	0	677	43289.73	43375.86	677	243	434	1863	1861
z3-BooledASS ^ne	0	569 (base -1516)	350.16	419.06	569	1	568	1971	449
Yices2	3	2469	27204.08	27512.64	2472	1215	1257	68	68
bitwuzla-dandelion-base ⁿ	0	2479	17537.81	17847.37	2479	1220	1259	61	61
Bitwuzla-SPFD-base ⁿ	0	2478	17140.26	17451.16	2478	1220	1258	62	62
Bitwuzla-MachBV-base ⁿ	0	2478	17194.38	17504.70	2478	1220	1258	62	62
cvc5-cvc5-xyz-base ⁿ	0	2374	76965.30	77267.86	2374	1186	1188	166	166
z3-BooledASS-base ⁿ	0	2085	93913.54	94177.03	2085	1101	984	455	455
Z3-GEX-base ⁿ	0	2084	84772.32	85040.98	2084	1101	983	456	456
Z3-alpha2-base ⁿ	0	2083	92928.81	93197.04	2083	1100	983	457	457

(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	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Bitwuzla-MachBV	0	2495 (base +17)	18732.06	19045.00	2495	1225	1270	45	45
Bitwuzla	0	2475	19066.80	19376.69	2475	1213	1262	65	65
bitwuzla-dandelion ⁿ	0	2472 (base -7)	181812.38	182137.12	2472	1221	1251	68	68
Bitwuzla-SPFD ^ne	0	2457 (base -21)	67200.71	67508.98	2457	1211	1246	83	83
bv_decide-nokernel	0	2404	128731.41	129084.44	2404	1180	1224	136	134
bv_decide	0	2401	157573.75	157937.31	2401	1179	1222	139	137
cvc5-cvc5-xyz ^ne	0	2375 (base +1)	77836.34	78137.09	2375	1187	1188	165	165
cvc5	0	2375	77951.89	78253.72	2375	1187	1188	165	165
NeuroSym	0	2358	7780.05	7513.73	2358	1162	1196	182	1
Z3-GEX	0	2294 (base +210)	272369.21	74108.80	2294	1119	1175	246	246
Z3-alpha2 ^ne	0	2131 (base +48)	93661.23	93568.24	2131	1128	1003	409	409
Z3-alpha2-debug ⁿ	0	2130	99868.38	97735.79	2130	1127	1003	410	410
SMTInterpol	0	1009	128723.30	99293.15	1009	160	849	1531	1300
Roole	0	677	43289.73	43375.86	677	243	434	1863	1861
z3-BooledASS ^ne	0	569 (base -1516)	350.16	419.06	569	1	568	1971	449
Yices2	3	2469	27204.08	27512.64	2472	1215	1257	68	68
bitwuzla-dandelion-base ⁿ	0	2479	17537.81	17847.37	2479	1220	1259	61	61
Bitwuzla-SPFD-base ⁿ	0	2478	17140.26	17451.16	2478	1220	1258	62	62
Bitwuzla-MachBV-base ⁿ	0	2478	17194.38	17504.70	2478	1220	1258	62	62
cvc5-cvc5-xyz-base ⁿ	0	2374	76965.30	77267.86	2374	1186	1188	166	166
z3-BooledASS-base ⁿ	0	2085	93913.54	94177.03	2085	1101	984	455	455
Z3-GEX-base ⁿ	0	2084	84772.32	85040.98	2084	1101	983	456	456
Z3-alpha2-base ⁿ	0	2083	92928.81	93197.04	2083	1100	983	457	457

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla-MachBV	0	1225 (base +5)	9068.61	9221.84	1225	1225	0	6	1309	6
bitwuzla-dandelion ⁿ	0	1221 (base +1)	13088.47	13242.37	1221	1221	0	10	1309	10
Bitwuzla	0	1213	9302.22	9453.83	1213	1213	0	18	1309	18
Bitwuzla-SPFD ^ne	0	1211 (base -9)	34539.88	34691.76	1211	1211	0	20	1309	20
cvc5-cvc5-xyz ^ne	0	1187 (base +1)	25610.00	25758.79	1187	1187	0	44	1309	44
cvc5	0	1187	25672.68	25821.97	1187	1187	0	44	1309	44
bv_decide-nokernel	0	1180	41695.85	41857.81	1180	1180	0	51	1309	50
bv_decide	0	1179	40274.97	40440.22	1179	1179	0	52	1309	51
NeuroSym	0	1162	3713.50	3580.87	1162	1162	0	69	1309	1
Z3-alpha2	0	1128 (base +28)	46459.56	46398.10	1128	1128	0	103	1309	103
Z3-alpha2-debug ⁿ	0	1127	49167.87	48027.43	1127	1127	0	104	1309	104
Z3-GEX	0	1119 (base +18)	134969.37	37235.72	1119	1119	0	112	1309	112
Roole	0	243	35112.47	35144.70	243	243	0	988	1309	988
SMTInterpol	0	160	30247.24	27428.52	160	160	0	1071	1309	909
z3-BooledASS ^ne	0	1 (base -1100)	0.16	0.28	1	1	0	1230	1309	124
Yices2	3	1214	12769.75	12921.98	1217	1214	3	14	1309	14
bitwuzla-dandelion-base ⁿ	0	1220	6743.44	6895.42	1220	1220	0	11	1309	11
Bitwuzla-SPFD-base ⁿ	0	1220	7005.34	7158.18	1220	1220	0	11	1309	11
Bitwuzla-MachBV-base ⁿ	0	1220	7071.75	7223.92	1220	1220	0	11	1309	11
cvc5-cvc5-xyz-base ⁿ	0	1186	24572.17	24721.87	1186	1186	0	45	1309	45
Z3-GEX-base ⁿ	0	1101	39325.36	39466.62	1101	1101	0	130	1309	130
z3-BooledASS-base ⁿ	0	1101	48264.86	48404.21	1101	1101	0	130	1309	130
Z3-alpha2-base ⁿ	0	1100	47494.39	47635.75	1100	1100	0	131	1309	131

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla-MachBV	1270 (base +12)	9663.44	9823.15	1270	1270	14	1256	14
Bitwuzla	1262	9764.58	9922.87	1262	1262	22	1256	22
Yices2	1254	14345.45	14501.64	1254	1254	30	1256	30
bitwuzla-dandelion ⁿ	1251 (base -8)	168723.92	168894.75	1251	1251	33	1256	33
Bitwuzla-SPFD ^ne	1246 (base -12)	32660.83	32817.21	1246	1246	38	1256	38
bv_decide-nokernel	1224	87035.57	87226.63	1224	1224	60	1256	59
bv_decide	1222	117298.78	117497.10	1222	1222	62	1256	61
NeuroSym	1196	4066.55	3932.86	1196	1196	88	1256	0
cvc5-cvc5-xyz ^ne	1188 (base +0)	52226.34	52378.30	1188	1188	96	1256	96
cvc5	1188	52279.21	52431.75	1188	1188	96	1256	96
Z3-GEX	1175 (base +192)	137399.84	36873.08	1175	1175	109	1256	109
Z3-alpha2 ^ne	1003 (base +20)	47201.67	47170.14	1003	1003	281	1256	281
Z3-alpha2-debug ⁿ	1003	50700.50	49708.36	1003	1003	281	1256	281
SMTInterpol	849	98476.06	71864.63	849	849	435	1256	374
z3-BooledASS ^ne	568 (base -416)	349.99	418.78	568	568	716	1256	300
Roole	434	8177.26	8231.16	434	434	850	1256	848
bitwuzla-dandelion-base ⁿ	1259	10794.37	10951.95	1259	1259	25	1256	25
Bitwuzla-MachBV-base ⁿ	1258	10122.63	10280.78	1258	1258	26	1256	26
Bitwuzla-SPFD-base ⁿ	1258	10134.93	10292.98	1258	1258	26	1256	26
cvc5-cvc5-xyz-base ⁿ	1188	52393.13	52545.99	1188	1188	96	1256	96
z3-BooledASS-base ⁿ	984	45648.67	45772.82	984	984	300	1256	300
Z3-alpha2-base ⁿ	983	45434.42	45561.29	983	983	301	1256	301
Z3-GEX-base ⁿ	983	45446.95	45574.37	983	983	301	1256	301

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla-MachBV ^ne	0	2401 (base +33)	4047.62	4347.30	2401	1186	1215	0	139
Bitwuzla	0	2385	3518.62	3815.07	2385	1169	1216	0	155
NeuroSym	0	2352	7614.35	7348.87	2352	1157	1195	125	63
Bitwuzla-SPFD ^ne	0	2135 (base -234)	9084.91	9348.54	2135	992	1143	0	405
cvc5	0	1997	6024.81	6271.62	1997	981	1016	0	543
cvc5-cvc5-xyz ^ne	0	1995 (base +2)	6023.76	6269.47	1995	980	1015	0	545
Z3-GEX ^ne	0	1962 (base +282)	15270.66	4971.68	1962	956	1006	0	578
bitwuzla-dandelion ⁿ	0	1959 (base -415)	4706.24	4950.30	1959	1143	816	0	581
Z3-alpha2 ^ne	0	1698 (base +19)	3926.92	4057.51	1698	904	794	0	842
Z3-alpha2-debug ⁿ	0	1694	10179.53	8687.76	1694	903	791	0	846
bv_decide-nokernel	0	1665	8331.65	8584.61	1665	900	765	1	874
bv_decide	0	1554	7739.81	7981.70	1554	902	652	1	985
z3-BooledASS ^ne	0	567 (base -1115)	253.36	322.00	567	1	566	1120	853
SMTInterpol	0	473	5489.38	2303.15	473	84	389	103	1964
Roole	0	470	1939.22	1997.17	470	60	410	0	2070
Yices2	3	2329	2979.78	3268.42	2332	1124	1208	0	208
bitwuzla-dandelion-base ⁿ	0	2374	3587.18	3882.23	2374	1172	1202	0	166
Bitwuzla-SPFD-base ⁿ	0	2369	3635.68	3931.46	2369	1171	1198	0	171
Bitwuzla-MachBV-base ⁿ	0	2368	3641.60	3936.55	2368	1170	1198	0	172
cvc5-cvc5-xyz-base ⁿ	0	1993	5981.14	6228.04	1993	978	1015	0	547
z3-BooledASS-base ⁿ	0	1682	3460.47	3666.31	1682	886	796	0	858
Z3-GEX-base ⁿ	0	1680	3414.41	3624.99	1680	891	789	0	860
Z3-alpha2-base ⁿ	0	1679	3302.14	3511.47	1679	886	793	0	861

SMT-COMP 2026