ABV (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 892
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	615	3561.12	3638.46	615	565	50	277	277
Bitwuzla-fixed ⁿ	615	3570.53	3647.09	615	565	50	277	277
cvc5-cvc5-xyz ^ne	538 (base +1)	39027.71	39097.91	538	355	183	354	138
cvc5	538	39630.49	39701.02	538	355	183	354	137
z3-BooledASS ^ne	167 (base -154)	1253.29	1273.80	167	139	28	725	33
SMTInterpol	138	5082.88	3800.33	138	17	121	754	59
UltimateEliminator+MathSAT	126	576.56	273.42	126	99	27	766	0
bitwuzla-dandelion ⁿ	124 (base +1)	39.95	55.46	124	121	3	768	30
cvc5-cvc5-xyz-base ⁿ	537	40346.30	40416.30	537	354	183	355	137
z3-BooledASS-base ⁿ	321	1781.08	1820.51	321	280	41	571	85
bitwuzla-dandelion-base ⁿ	123	37.13	52.47	123	120	3	769	31

(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	615	3561.12	3638.46	615	565	50	277	277
Bitwuzla-fixed ⁿ	615	3570.53	3647.09	615	565	50	277	277
cvc5-cvc5-xyz ^ne	538 (base +1)	39027.71	39097.91	538	355	183	354	138
cvc5	538	39630.49	39701.02	538	355	183	354	137
z3-BooledASS ^ne	167 (base -154)	1253.29	1273.80	167	139	28	725	33
SMTInterpol	138	5082.88	3800.33	138	17	121	754	59
UltimateEliminator+MathSAT	126	576.56	273.42	126	99	27	766	0
bitwuzla-dandelion ⁿ	124 (base +1)	39.95	55.46	124	121	3	768	30
cvc5-cvc5-xyz-base ⁿ	537	40346.30	40416.30	537	354	183	355	137
z3-BooledASS-base ⁿ	321	1781.08	1820.51	321	280	41	571	85
bitwuzla-dandelion-base ⁿ	123	37.13	52.47	123	120	3	769	31

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla-fixed ⁿ	565	3023.84	3094.12	565	565	77	250	77
Bitwuzla	565	3028.87	3099.93	565	565	77	250	77
cvc5	355	19476.19	19522.16	355	355	287	250	109
cvc5-cvc5-xyz ^ne	355 (base +1)	20022.72	20068.64	355	355	287	250	110
z3-BooledASS ^ne	139 (base -141)	1160.19	1177.26	139	139	503	250	13
bitwuzla-dandelion ⁿ	121 (base +1)	21.11	36.23	121	121	521	250	15
UltimateEliminator+MathSAT	99	451.47	214.86	99	99	543	250	0
SMTInterpol	17	17.43	11.91	17	17	625	250	53
cvc5-cvc5-xyz-base ⁿ	354	20024.65	20070.11	354	354	288	250	109
z3-BooledASS-base ⁿ	280	1678.80	1713.22	280	280	362	250	28
bitwuzla-dandelion-base ⁿ	120	18.48	33.43	120	120	522	250	15

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	183 (base +0)	19004.99	19029.27	183	183	18	691	14
cvc5	183	20154.29	20178.87	183	183	18	691	14
SMTInterpol	121	5065.45	3788.42	121	121	80	691	3
Bitwuzla	50	532.25	538.54	50	50	151	691	151
Bitwuzla-fixed ⁿ	50	546.69	552.98	50	50	151	691	151
z3-BooledASS ^ne	28 (base -13)	93.10	96.54	28	28	173	691	5
UltimateEliminator+MathSAT	27	125.08	58.56	27	27	174	691	0
bitwuzla-dandelion ⁿ	3 (base +0)	18.84	19.23	3	3	198	691	3
cvc5-cvc5-xyz-base ⁿ	183	20321.66	20346.19	183	183	18	691	14
z3-BooledASS-base ⁿ	41	102.28	107.29	41	41	160	691	34
bitwuzla-dandelion-base ⁿ	3	18.65	19.04	3	3	198	691	3

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla	592	504.72	578.37	592	545	47	0	300
Bitwuzla-fixed ⁿ	592	507.70	580.70	592	545	47	0	300
cvc5-cvc5-xyz ^ne	254 (base +10)	139.56	170.76	254	185	69	2	636
cvc5	244	132.03	162.24	244	184	60	2	646
z3-BooledASS ^ne	164 (base -151)	48.53	68.59	164	137	27	683	45
UltimateEliminator+MathSAT	126	576.56	273.42	126	99	27	766	0
bitwuzla-dandelion ⁿ	124 (base +1)	39.95	55.46	124	121	3	737	31
SMTInterpol	124	149.06	90.06	124	17	107	630	138
z3-BooledASS-base ⁿ	315	120.35	158.85	315	275	40	478	99
cvc5-cvc5-xyz-base ⁿ	244	145.91	175.94	244	184	60	2	646
bitwuzla-dandelion-base ⁿ	123	37.13	52.47	123	120	3	738	31

SMT-COMP 2026