SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_Equality_Bitvec (Single Query Track)

Competition results for the QF_Equality_Bitvec division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

QF_ABV : 7574 benchmarks
QF_AUFBV : 75 benchmarks
QF_UFBV : 764 benchmarks
QF_UFBVDT : 76 benchmarks

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	8279	27920.69	28953.07	8279	5416	2863	134	76	132	2
Yices2	0	8230	71312.92	72346.37	8230	5411	2819	183	76	182	1
Z3-Owl	0	8056 (base +182)	99548.31	100577.24	8056	5312	2744	357	76	301	28
cvc5	0	8009	293515.59	294553.59	8009	5260	2749	480	0	395	83
SMTInterpol	0	6442	399199.02	347593.54	6453	3976	2477	2036	0	1797	0
Z3-Owl-base ⁿ	0	7874	90158.59	91142.29	7874	5277	2597	539	76	535	4

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	8279	27920.69	28953.07	8279	5416	2863	134	76	132	2
Yices2	0	8230	71312.92	72346.37	8230	5411	2819	183	76	182	1
Z3-Owl	0	8056 (base +182)	99548.31	100577.24	8056	5312	2744	357	76	301	28
cvc5	0	8009	293515.59	294553.59	8009	5260	2749	480	0	395	83
SMTInterpol	0	6453	413241.74	360487.89	6453	3976	2477	2036	0	1797	0
Z3-Owl-base ⁿ	0	7874	90158.59	91142.29	7874	5277	2597	539	76	535	4

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	5416	12534.36	13208.61	5416	5416	0	6	3067	4	2
Yices2	0	5411	31070.94	31748.18	5411	5411	0	11	3067	10	1
Z3-Owl	0	5312 (base +35)	34911.75	35586.70	5312	5312	0	110	3067	97	4
cvc5	0	5260	118715.24	119381.79	5260	5260	0	202	3027	165	36
SMTInterpol	0	3976	323230.20	285768.88	3976	3976	0	1486	3027	1304	0
Z3-Owl-base ⁿ	0	5277	50083.74	50741.20	5277	5277	0	145	3067	144	1

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

UNSAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	2863	15386.34	15744.46	2863	0	2863	77	5549	77	0
Yices2	0	2819	40241.98	40598.18	2819	0	2819	121	5549	121	0
cvc5	0	2749	174800.35	175171.80	2749	0	2749	197	5543	173	23
Z3-Owl	0	2744 (base +147)	64636.56	64990.54	2744	0	2744	196	5549	163	19
SMTInterpol	0	2477	90011.54	74719.01	2477	0	2477	469	5543	457	0
Z3-Owl-base ⁿ	0	2597	40074.85	40401.09	2597	0	2597	343	5549	343	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	8090	9829.84	10835.10	8090	5285	2805	0	399	0	0
Yices2	0	7879	5536.43	6517.07	7879	5287	2592	0	610	0	0
Z3-Owl	0	7706 (base +282)	12036.32	13009.40	7706	5197	2509	0	783	0	0
cvc5	0	6978	8937.21	9799.98	6978	4705	2273	2	1509	0	0
SMTInterpol	0	5112	28233.85	12419.02	5112	2904	2208	137	3240	0	0
Z3-Owl-base ⁿ	0	7424	4630.43	5546.58	7424	5096	2328	0	1065	0	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver