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

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Bitwuzla	Bitwuzla	STP	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	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 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 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 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 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