SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_Bitvec (Model Validation Track)

Competition results for the QF_Bitvec division in the Model Validation Track. Chart

Results were generated on 2025-08-11

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

Logics:

QF_BV : 8211 benchmarks

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	8166	38291.19	39296.71	8166	8166	45	0	39	4
Yices2	0	8121	73011.21	74029.36	8121	8121	90	0	89	0
cvc5	0	8049	118478.39	119484.19	8049	8049	162	0	149	12
SMTInterpol	0	3878	192678.88	166115.10	3887	3887	4324	0	3525	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	8166	38291.19	39296.71	8166	8166	45	0	39	4
Yices2	0	8121	73011.21	74029.36	8121	8121	90	0	89	0
cvc5	0	8049	118478.39	119484.19	8049	8049	162	0	149	12
SMTInterpol	0	3887	203622.49	176633.66	3887	3887	4324	0	3525	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	8166	38291.19	39296.71	8166	8166	45	0	39	4
Yices2	0	8121	73011.21	74029.36	8121	8121	90	0	89	0
cvc5	0	8049	118478.39	119484.19	8049	8049	162	0	149	12
SMTInterpol	0	3887	203622.49	176633.66	3887	3887	4324	0	3525	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	7994	8678.44	9656.84	7994	7994	0	217	0	0
Yices2	0	7738	6171.97	7132.82	7738	7738	0	473	0	0
cvc5	0	7271	14982.41	15875.25	7271	7271	0	940	0	0
SMTInterpol	0	3164	19399.80	9266.46	3164	3164	321	4726	0	0