QF_Bitvec (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

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

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Bitwuzla-MachBV	10523 (base +38)	97390.14	98711.15	10523	4929	5594	180	179	1
Bitwuzla	10498	100202.01	101517.47	10498	4931	5567	205	203	2
Yices2	10491	120555.40	121864.36	10491	4924	5567	212	211	1
cvc5	9938	302092.27	303362.99	9938	4790	5148	765	727	32
z3siri	9308 (base +364)	429081.45	430296.03	9308	4435	4873	1395	1204	11
Z3-alpha	8970 (base +25)	544609.75	144055.13	9370	4592	4778	1333	1254	76
bv_decide-nokernel	8862	426162.80	427483.91	8862	4713	4149	1841	1802	37
Z3-Owl	8656 (base +115)	345612.16	346754.50	8656	4501	4155	2047	2031	9
bv_decide	8638	638058.46	639387.52	8638	4627	4011	2065	2025	37
SMTInterpol	2917	337337.08	303061.00	2925	596	2329	7778	6807	0
Bitwuzla-MachBV-base ⁿ	10485	113665.37	114969.55	10485	4928	5557	218	213	5
Z3-alpha-base ⁿ	8945	389801.87	390962.90	8945	4467	4478	1758	1746	10
z3siri-base ⁿ	8944	391867.14	393027.61	8944	4467	4477	1759	1747	10
Z3-Owl-base ⁿ	8541	587768.50	588896.66	8541	4281	4260	2162	2152	8

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

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Bitwuzla-MachBV	10523 (base +38)	97390.14	98711.15	10523	4929	5594	180	179	1
Bitwuzla	10498	100202.01	101517.47	10498	4931	5567	205	203	2
Yices2	10491	120555.40	121864.36	10491	4924	5567	212	211	1
cvc5	9938	302092.27	303362.99	9938	4790	5148	765	727	32
Z3-alpha	9370 (base +425)	1532034.50	393050.52	9370	4592	4778	1333	1254	76
z3siri	9308 (base +364)	429081.45	430296.03	9308	4435	4873	1395	1204	11
bv_decide-nokernel	8862	426162.80	427483.91	8862	4713	4149	1841	1802	37
Z3-Owl	8656 (base +115)	345612.16	346754.50	8656	4501	4155	2047	2031	9
bv_decide	8638	638058.46	639387.52	8638	4627	4011	2065	2025	37
SMTInterpol	2925	347054.64	312426.58	2925	596	2329	7778	6807	0
Bitwuzla-MachBV-base ⁿ	10485	113665.37	114969.55	10485	4928	5557	218	213	5
Z3-alpha-base ⁿ	8945	389801.87	390962.90	8945	4467	4478	1758	1746	10
z3siri-base ⁿ	8944	391867.14	393027.61	8944	4467	4477	1759	1747	10
Z3-Owl-base ⁿ	8541	587768.50	588896.66	8541	4281	4260	2162	2152	8

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

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	4931	44557.48	45173.98	4931	4931	31	5741	29	2
Bitwuzla-MachBV	4929 (base +1)	50034.86	50653.33	4929	4929	33	5741	32	1
Yices2	4924	50873.51	51487.19	4924	4924	38	5741	37	1
cvc5	4790	109431.02	110037.61	4790	4790	172	5741	157	11
bv_decide-nokernel	4713	210107.19	210776.11	4713	4713	249	5741	244	4
bv_decide	4627	290823.50	291487.41	4627	4627	335	5741	331	3
Z3-alpha	4592 (base +125)	681224.03	176140.63	4592	4592	370	5741	361	9
Z3-Owl	4501 (base +220)	161409.09	162001.11	4501	4501	461	5741	454	4
z3siri	4435 (base -32)	209098.46	209677.25	4435	4435	527	5741	425	9
SMTInterpol	596	127475.21	116503.29	596	596	4366	5741	3684	0
Bitwuzla-MachBV-base ⁿ	4928	53134.81	53747.05	4928	4928	34	5741	29	5
Z3-alpha-base ⁿ	4467	199624.27	200203.84	4467	4467	495	5741	489	6
z3siri-base ⁿ	4467	201216.42	201797.38	4467	4467	495	5741	489	6
Z3-Owl-base ⁿ	4281	326455.94	327025.02	4281	4281	681	5741	675	6

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

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla-MachBV	5594 (base +37)	47355.28	48057.82	5594	5594	52	5057	52	0
Bitwuzla	5567	55644.53	56343.49	5567	5567	79	5057	79	0
Yices2	5567	69681.89	70377.17	5567	5567	79	5057	79	0
cvc5	5148	192661.24	193325.38	5148	5148	498	5057	481	15
z3siri	4873 (base +396)	219982.99	220618.78	4873	4873	773	5057	686	2
Z3-alpha	4778 (base +300)	850810.48	216909.89	4778	4778	868	5057	829	36
Z3-Owl	4155 (base -105)	184203.06	184753.39	4155	4155	1491	5057	1488	0
bv_decide-nokernel	4149	216055.61	216707.80	4149	4149	1497	5057	1464	32
bv_decide	4011	347234.96	347900.11	4011	4011	1635	5057	1599	34
SMTInterpol	2329	219579.43	195923.30	2329	2329	3317	5057	3051	0
Bitwuzla-MachBV-base ⁿ	5557	60530.55	61222.50	5557	5557	89	5057	89	0
Z3-alpha-base ⁿ	4478	190177.61	190759.06	4478	4478	1168	5057	1164	2
z3siri-base ⁿ	4477	190650.72	191230.23	4477	4477	1169	5057	1165	2
Z3-Owl-base ⁿ	4260	261312.56	261871.64	4260	4260	1386	5057	1383	1

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

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla-MachBV	10101 (base +118)	17784.17	19040.53	10101	4743	5358	0	602
Bitwuzla	10019	14109.70	15349.90	10019	4728	5291	0	684
Yices2	9909	11127.29	12349.05	9909	4589	5320	0	794
cvc5	8498	24252.34	25300.07	8498	4005	4493	1	2204
Z3-alpha	7734 (base +383)	70113.72	21374.05	7734	3795	3939	0	2969
z3siri	7387 (base +43)	19789.88	20708.35	7387	3487	3900	8	3308
Z3-Owl	6983 (base +512)	33022.68	33910.41	6983	3519	3464	0	3720
bv_decide-nokernel	6049	34413.15	35348.33	6049	3181	2868	1	4653
bv_decide	5694	37930.67	38815.86	5694	3010	2684	1	5008
SMTInterpol	1965	21583.01	9183.17	1965	287	1678	423	8315
Bitwuzla-MachBV-base ⁿ	9983	16027.77	17255.32	9983	4716	5267	0	720
Z3-alpha-base ⁿ	7351	17648.29	18560.45	7351	3615	3736	0	3352
z3siri-base ⁿ	7344	17741.41	18651.46	7344	3612	3732	0	3359
Z3-Owl-base ⁿ	6471	22159.50	22960.32	6471	3169	3302	0	4232

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

SMT-COMP 2025