BV (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 608
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 ⁿ	559	4071.39	4140.29	559	147	412	49	43
Bitwuzla	557	4047.69	4117.22	557	147	410	51	45
cvc5	552	19829.73	19900.30	552	134	418	56	50
cvc5-cvc5-xyz ^ne	552 (base +0)	19839.94	19910.20	552	134	418	56	50
YicesQS	526	10417.70	10477.02	526	141	385	82	76
bitwuzla-dandelion ⁿ	467 (base -18)	5612.68	5671.36	467	135	332	141	112
z3-BooledASS ^ne	452 (base +0)	5535.43	5591.41	452	122	330	156	146
UltimateEliminator+MathSAT	189	2961.09	2405.43	189	17	172	419	91
SMTInterpol	164	179.34	107.84	164	1	163	444	101
cvc5-cvc5-xyz-base ⁿ	552	19838.07	19908.67	552	134	418	56	50
bitwuzla-dandelion-base ⁿ	485	5284.68	5345.32	485	148	337	123	117
z3-BooledASS-base ⁿ	452	7441.10	7497.41	452	121	331	156	145

(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 ⁿ	559	4071.39	4140.29	559	147	412	49	43
Bitwuzla	557	4047.69	4117.22	557	147	410	51	45
cvc5	552	19829.73	19900.30	552	134	418	56	50
cvc5-cvc5-xyz ^ne	552 (base +0)	19839.94	19910.20	552	134	418	56	50
YicesQS	526	10417.70	10477.02	526	141	385	82	76
bitwuzla-dandelion ⁿ	467 (base -18)	5612.68	5671.36	467	135	332	141	112
z3-BooledASS ^ne	452 (base +0)	5535.43	5591.41	452	122	330	156	146
UltimateEliminator+MathSAT	189	2961.09	2405.43	189	17	172	419	91
SMTInterpol	164	179.34	107.84	164	1	163	444	101
cvc5-cvc5-xyz-base ⁿ	552	19838.07	19908.67	552	134	418	56	50
bitwuzla-dandelion-base ⁿ	485	5284.68	5345.32	485	148	337	123	117
z3-BooledASS-base ⁿ	452	7441.10	7497.41	452	121	331	156	145

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla	147	739.90	758.31	147	147	13	448	7
Bitwuzla-fixed ⁿ	147	745.32	763.46	147	147	13	448	7
YicesQS	141	4533.38	4546.31	141	141	19	448	13
bitwuzla-dandelion ⁿ	135 (base -13)	1075.71	1092.63	135	135	25	448	3
cvc5	134	9636.03	9653.80	134	134	26	448	20
cvc5-cvc5-xyz ^ne	134 (base +0)	9646.13	9663.66	134	134	26	448	20
z3-BooledASS ^ne	122 (base +1)	284.38	299.40	122	122	38	448	30
UltimateEliminator+MathSAT	17	808.69	689.65	17	17	143	448	58
SMTInterpol	1	1.06	0.63	1	1	159	448	60
bitwuzla-dandelion-base ⁿ	148	660.04	678.37	148	148	12	448	6
cvc5-cvc5-xyz-base ⁿ	134	9640.77	9658.34	134	134	26	448	20
z3-BooledASS-base ⁿ	121	317.21	332.07	121	121	39	448	30

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	418	10193.70	10246.49	418	418	19	171	19
cvc5-cvc5-xyz ^ne	418 (base +0)	10193.81	10246.54	418	418	19	171	19
Bitwuzla-fixed ⁿ	412	3326.07	3376.83	412	412	25	171	25
Bitwuzla	410	3307.79	3358.90	410	410	27	171	27
YicesQS	385	5884.32	5930.72	385	385	52	171	52
bitwuzla-dandelion ⁿ	332 (base -5)	4536.96	4578.73	332	332	105	171	99
z3-BooledASS ^ne	330 (base -1)	5251.05	5292.01	330	330	107	171	107
UltimateEliminator+MathSAT	172	2152.41	1715.77	172	172	265	171	26
SMTInterpol	163	178.28	107.21	163	163	274	171	35
cvc5-cvc5-xyz-base ⁿ	418	10197.31	10250.32	418	418	19	171	19
bitwuzla-dandelion-base ⁿ	337	4624.65	4666.94	337	337	100	171	100
z3-BooledASS-base ⁿ	331	7123.89	7165.34	331	331	106	171	106

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla-fixed ⁿ	543	375.26	441.52	543	141	402	6	59
Bitwuzla	540	357.89	424.71	540	141	399	6	62
YicesQS	496	293.62	354.66	496	123	373	6	106
bitwuzla-dandelion ⁿ	446 (base -11)	468.56	524.05	446	131	315	29	133
z3-BooledASS ^ne	420 (base -1)	216.32	267.89	420	118	302	6	182
cvc5	403	702.30	752.38	403	42	361	6	199
cvc5-cvc5-xyz ^ne	402 (base +0)	681.81	731.51	402	42	360	6	200
UltimateEliminator+MathSAT	184	966.96	473.95	184	15	169	307	117
SMTInterpol	164	179.34	107.84	164	1	163	308	136
bitwuzla-dandelion-base ⁿ	457	428.02	484.63	457	143	314	6	145
z3-BooledASS-base ⁿ	421	275.52	327.19	421	117	304	6	181
cvc5-cvc5-xyz-base ⁿ	402	684.91	734.83	402	42	360	6	200

SMT-COMP 2026