AUFBV (Single Query Track)

Competition results for the AUFBV 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 ⁿ	374 (base +0)	19255.23	19304.86	374	114	260	178	172
Bitwuzla	371	19262.65	19312.87	371	116	255	181	176
Bitwuzla-fixed ⁿ	371	19593.82	19643.60	371	116	255	181	176
z3-BooledASS ^ne	195 (base +3)	12955.48	12980.82	195	67	128	357	330
cvc5	155	28644.88	28666.51	155	8	147	397	325
cvc5-cvc5-xyz ^ne	141 (base -4)	22673.67	22693.08	141	8	133	411	321
SMTInterpol	24	7248.76	6554.67	24	0	24	528	427
UltimateEliminator+MathSAT	4	73.07	40.43	4	0	4	548	215
bitwuzla-dandelion-base ⁿ	374	21230.44	21280.82	374	115	259	178	173
z3-BooledASS-base ⁿ	192	13953.50	13978.57	192	63	129	360	326
cvc5-cvc5-xyz-base ⁿ	145	24174.82	24194.91	145	8	137	407	325

(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 ⁿ	374 (base +0)	19255.23	19304.86	374	114	260	178	172
Bitwuzla	371	19262.65	19312.87	371	116	255	181	176
Bitwuzla-fixed ⁿ	371	19593.82	19643.60	371	116	255	181	176
z3-BooledASS ^ne	195 (base +3)	12955.48	12980.82	195	67	128	357	330
cvc5	155	28644.88	28666.51	155	8	147	397	325
cvc5-cvc5-xyz ^ne	141 (base -4)	22673.67	22693.08	141	8	133	411	321
SMTInterpol	24	7248.76	6554.67	24	0	24	528	427
UltimateEliminator+MathSAT	4	73.07	40.43	4	0	4	548	215
bitwuzla-dandelion-base ⁿ	374	21230.44	21280.82	374	115	259	178	173
z3-BooledASS-base ⁿ	192	13953.50	13978.57	192	63	129	360	326
cvc5-cvc5-xyz-base ⁿ	145	24174.82	24194.91	145	8	137	407	325

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla	116	3554.36	3569.47	116	116	5	431	5
Bitwuzla-fixed ⁿ	116	4023.00	4037.97	116	116	5	431	5
bitwuzla-dandelion ⁿ	114 (base -1)	3325.86	3340.56	114	114	7	431	6
z3-BooledASS ^ne	67 (base +4)	2197.84	2206.28	67	67	54	431	50
cvc5-cvc5-xyz ^ne	8 (base +0)	1762.84	1763.95	8	8	113	431	52
cvc5	8	2019.82	2020.92	8	8	113	431	59
SMTInterpol	0	0.00	0.00	0	0	121	431	62
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	121	431	98
bitwuzla-dandelion-base ⁿ	115	3400.14	3415.12	115	115	6	431	6
z3-BooledASS-base ⁿ	63	2232.50	2240.58	63	63	58	431	46
cvc5-cvc5-xyz-base ⁿ	8	2021.54	2022.67	8	8	113	431	59

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
bitwuzla-dandelion ⁿ	260 (base +1)	15929.37	15964.29	260	260	18	274	18
Bitwuzla-fixed ⁿ	255	15570.82	15605.64	255	255	23	274	23
Bitwuzla	255	15708.29	15743.41	255	255	23	274	23
cvc5	147	26625.07	26645.59	147	147	131	274	119
cvc5-cvc5-xyz ^ne	133 (base -4)	20910.83	20929.12	133	133	145	274	121
z3-BooledASS ^ne	128 (base -1)	10757.64	10774.54	128	128	150	274	141
SMTInterpol	24	7248.76	6554.67	24	24	254	274	226
UltimateEliminator+MathSAT	4	73.07	40.43	4	4	274	274	89
bitwuzla-dandelion-base ⁿ	259	17830.30	17865.69	259	259	19	274	19
cvc5-cvc5-xyz-base ⁿ	137	22153.28	22172.24	137	137	141	274	119
z3-BooledASS-base ⁿ	129	11721.00	11737.99	129	129	149	274	142

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla-fixed ⁿ	296	870.75	907.39	296	105	191	5	251
Bitwuzla	296	880.60	917.38	296	105	191	5	251
bitwuzla-dandelion ⁿ	290 (base -7)	847.48	883.77	290	103	187	6	256
z3-BooledASS	140 (base -1)	463.07	480.35	140	53	87	9	403
cvc5	107	460.67	473.91	107	2	105	6	439
cvc5-cvc5-xyz ^ne	100 (base -1)	421.64	434.05	100	2	98	10	442
SMTInterpol	8	172.06	69.93	8	0	8	32	512
UltimateEliminator+MathSAT	3	30.13	11.37	3	0	3	323	226
bitwuzla-dandelion-base ⁿ	297	896.72	933.88	297	106	191	5	250
z3-BooledASS-base ⁿ	141	527.35	544.79	141	51	90	12	399
cvc5-cvc5-xyz-base ⁿ	101	415.43	427.87	101	2	99	11	440

SMT-COMP 2026