BVFPLRA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 266
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	266	59.88	92.79	266	241	25	0	0
Bitwuzla-fixed ⁿ	266	60.30	93.01	266	241	25	0	0
cvc5	262	1329.08	1361.46	262	237	25	4	4
cvc5-cvc5-xyz ^ne	262 (base +0)	1334.91	1367.28	262	237	25	4	4
colibri2	69	14.23	22.66	69	53	16	197	10
UltimateEliminator+MathSAT	15	95.10	61.01	15	12	3	251	0
bitwuzla-dandelion ⁿ	0 (base -256)	0.00	0.00	0	0	0	266	0
z3-BooledASS ^ne	0 (base -250)	0.00	0.00	0	0	0	266	0
cvc5-cvc5-xyz-base ⁿ	262	1336.28	1368.82	262	237	25	4	4
bitwuzla-dandelion-base ⁿ	256	174.47	206.38	256	231	25	10	10
z3-BooledASS-base ⁿ	250	5040.80	5071.97	250	225	25	16	13

(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	266	59.88	92.79	266	241	25	0	0
Bitwuzla-fixed ⁿ	266	60.30	93.01	266	241	25	0	0
cvc5	262	1329.08	1361.46	262	237	25	4	4
cvc5-cvc5-xyz ^ne	262 (base +0)	1334.91	1367.28	262	237	25	4	4
colibri2	69	14.23	22.66	69	53	16	197	10
UltimateEliminator+MathSAT	15	95.10	61.01	15	12	3	251	0
bitwuzla-dandelion ⁿ	0 (base -256)	0.00	0.00	0	0	0	266	0
z3-BooledASS ^ne	0 (base -250)	0.00	0.00	0	0	0	266	0
cvc5-cvc5-xyz-base ⁿ	262	1336.28	1368.82	262	237	25	4	4
bitwuzla-dandelion-base ⁿ	256	174.47	206.38	256	231	25	10	10
z3-BooledASS-base ⁿ	250	5040.80	5071.97	250	225	25	16	13

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla	241	54.14	83.98	241	241	0	25	0
Bitwuzla-fixed ⁿ	241	54.52	84.15	241	241	0	25	0
cvc5	237	1311.29	1340.60	237	237	4	25	4
cvc5-cvc5-xyz ^ne	237 (base +0)	1316.96	1346.25	237	237	4	25	4
colibri2	53	11.30	17.77	53	53	188	25	10
UltimateEliminator+MathSAT	12	78.90	51.20	12	12	229	25	0
bitwuzla-dandelion ⁿ	0 (base -231)	0.00	0.00	0	0	241	25	0
z3-BooledASS ^ne	0 (base -225)	0.00	0.00	0	0	241	25	0
cvc5-cvc5-xyz-base ⁿ	237	1318.32	1347.78	237	237	4	25	4
bitwuzla-dandelion-base ⁿ	231	48.93	77.70	231	231	10	25	10
z3-BooledASS-base ⁿ	225	3510.39	3538.32	225	225	16	25	13

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained
Bitwuzla	25	5.74	8.81	25	25	0	241
Bitwuzla-fixed ⁿ	25	5.78	8.86	25	25	0	241
cvc5	25	17.79	20.85	25	25	0	241
cvc5-cvc5-xyz ^ne	25 (base +0)	17.94	21.03	25	25	0	241
colibri2	16	2.93	4.88	16	16	9	241
UltimateEliminator+MathSAT	3	16.20	9.81	3	3	22	241
bitwuzla-dandelion ⁿ	0 (base -25)	0.00	0.00	0	0	25	241
z3-BooledASS ^ne	0 (base -25)	0.00	0.00	0	0	25	241
cvc5-cvc5-xyz-base ⁿ	25	17.96	21.04	25	25	0	241
bitwuzla-dandelion-base ⁿ	25	125.54	128.68	25	25	0	241
z3-BooledASS-base ⁿ	25	1530.41	1533.65	25	25	0	241

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla	266	59.88	92.79	266	241	25	0	0
Bitwuzla-fixed ⁿ	266	60.30	93.01	266	241	25	0	0
cvc5	260	128.56	160.58	260	235	25	0	6
cvc5-cvc5-xyz ^ne	260 (base +0)	134.41	166.41	260	235	25	0	6
colibri2	69	14.23	22.66	69	53	16	187	10
UltimateEliminator+MathSAT	15	95.10	61.01	15	12	3	251	0
bitwuzla-dandelion ⁿ	0 (base -255)	0.00	0.00	0	0	0	266	0
z3-BooledASS ^ne	0 (base -218)	0.00	0.00	0	0	0	266	0
cvc5-cvc5-xyz-base ⁿ	260	135.84	167.95	260	235	25	0	6
bitwuzla-dandelion-base ⁿ	255	54.45	86.21	255	231	24	0	11
z3-BooledASS-base ⁿ	218	440.31	467.07	218	204	14	3	45

SMT-COMP 2026