SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2024

QF_Bitvec (Single Query Track)

Competition results for the QF_Bitvec division in the Single Query Track.

Results were generated on 2024-07-08

Benchmarks: 10703
Time Limit: 1200 seconds
Memory Limit: 20480 GB

Logics:

QF_BV : 10703 benchmarks

Winners

winner_seq	winner_par	winner_sat	winner_unsat	winner_24s
Bitwuzla	Bitwuzla	STP	Bitwuzla	Bitwuzla

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	10489	136684.154526	137761.630559	10489	4907	5582	214	0	211	3
STP	0	10488	169828.228527	170916.15918	10488	4919	5569	215	0	212	0
Yices2	0	10388	142271.512368	143339.280115	10388	4862	5526	315	0	312	3
cvc5	0	9958	365361.544544	366433.45916	9958	4773	5185	745	0	712	32
Z3-alpha	0	9020	391942.581441	392924.173499	9020	4427	4593	1683	0	1664	9
SMTInterpol	0	3339	552128.65738	442522.52297	3548	842	2706	7155	0	6317	134

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	10489	136684.154526	137761.630559	10489	4907	5582	214	0	211	3
STP	0	10488	169828.228527	170916.15918	10488	4919	5569	215	0	212	0
Yices2	0	10388	142271.512368	143339.280115	10388	4862	5526	315	0	312	3
cvc5	0	9958	365361.544544	366433.45916	9958	4773	5185	745	0	712	32
Z3-alpha	0	9020	391942.581441	392924.173499	9020	4427	4593	1683	0	1664	9
SMTInterpol	0	3548	852576.881037	651070.952027	3548	842	2706	7155	0	6317	134

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
STP	0	4919	58214.949551	58719.496163	4919	4919	0	38	5746	35	0
Bitwuzla	0	4907	64503.779278	65008.447599	4907	4907	0	50	5746	48	2
Yices2	0	4862	64401.745312	64902.948059	4862	4862	0	95	5746	92	3
cvc5	0	4773	125866.620821	126372.253722	4773	4773	0	184	5746	170	13
Z3-alpha	0	4427	187187.975681	187666.416901	4427	4427	0	530	5746	527	3
SMTInterpol	0	842	161463.213932	143147.058681	842	842	0	4115	5746	3454	104

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	5582	72180.375248	72753.18296	5582	0	5582	75	5046	74	1
STP	0	5569	111613.278976	112196.663017	5569	0	5569	88	5046	88	0
Yices2	0	5526	77869.767056	78436.332056	5526	0	5526	131	5046	131	0
cvc5	0	5185	239494.923723	240061.205438	5185	0	5185	472	5046	457	15
Z3-alpha	0	4593	204754.60576	205257.756598	4593	0	4593	1064	5046	1049	5
SMTInterpol	0	2706	691113.667105	507923.893346	2706	0	2706	2951	5046	2793	22

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	9778	17874.335067	18855.879781	9778	4523	5255	0	925	0	0
Yices2	0	9743	11024.846841	12001.68132	9743	4482	5261	0	960	0	0
STP	0	9035	23227.666979	24136.900221	9035	4581	4454	0	1668	0	0
cvc5	0	8353	27196.665426	28037.397159	8353	3966	4387	0	2350	0	0
Z3-alpha	0	7170	15231.434193	15953.982852	7170	3580	3590	0	3533	0	0
SMTInterpol	0	2037	32731.166151	13363.052275	2037	392	1645	362	8304	0	0