SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_ADT_BitVec (Model Validation Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_ABV : 5214 benchmarks
QF_AUFBV : 25 benchmarks
QF_UFBVDT : 10 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	5226	3265.60	3900.44	5226	5226	13	10	3	1
cvc5	0	4771	68365.87	68960.10	4771	4771	478	0	468	7
SMTInterpol	0	3886	307681.94	272191.10	3898	3898	1351	0	1259	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	5226	3265.60	3900.44	5226	5226	13	10	3	1
cvc5	0	4771	68365.87	68960.10	4771	4771	478	0	468	7
SMTInterpol	0	3898	322296.69	286326.88	3898	3898	1351	0	1259	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	5226	3265.60	3900.44	5226	5226	13	10	3	1
cvc5	0	4771	68365.87	68960.10	4771	4771	478	0	468	7
SMTInterpol	0	3898	322296.69	286326.88	3898	3898	1351	0	1259	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	5204	1296.26	1927.97	5204	5204	6	39	0	0
cvc5	0	4220	5834.45	6351.07	4220	4220	3	1026	0	0
SMTInterpol	0	2846	13504.66	5898.18	2846	2846	37	2366	0	0