SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_ABV (Single Query Track)

Competition results for the QF_ABV logic in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Bitwuzla	Bitwuzla	Bitwuzla	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	7555	9266.28	10205.41	7555	5191	2364	19	0	18	1
Yices2	0	7546	12646.28	13586.79	7546	5190	2356	28	0	28	0
Z3-Owl	0	7472 (base +39)	35396.77	36343.43	7472	5143	2329	102	0	97	4
cvc5	0	7337	91241.19	92160.09	7337	5043	2294	237	0	235	2
SMTInterpol	0	5804	373574.53	331043.61	5815	3878	1937	1759	0	1676	0
Z3-Owl-base ⁿ	0	7433	38195.63	39117.90	7433	5117	2316	141	0	140	1

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

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	7555	9266.28	10205.41	7555	5191	2364	19	0	18	1
Yices2	0	7546	12646.28	13586.79	7546	5190	2356	28	0	28	0
Z3-Owl	0	7472 (base +39)	35396.77	36343.43	7472	5143	2329	102	0	97	4
cvc5	0	7337	91241.19	92160.09	7337	5043	2294	237	0	235	2
SMTInterpol	0	5815	387617.25	343937.96	5815	3878	1937	1759	0	1676	0
Z3-Owl-base ⁿ	0	7433	38195.63	39117.90	7433	5117	2316	141	0	140	1

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

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	5191	3458.09	4102.64	5191	5191	0	4	2379	3	1
Yices2	0	5190	5593.86	6240.03	5190	5190	0	5	2379	5	0
Z3-Owl	0	5143 (base +26)	24200.72	24852.56	5143	5143	0	52	2379	49	2
cvc5	0	5043	77801.80	78434.68	5043	5043	0	152	2379	150	2
SMTInterpol	0	3878	314359.05	278408.39	3878	3878	0	1317	2379	1244	0
Z3-Owl-base ⁿ	0	5117	26026.49	26661.17	5117	5117	0	78	2379	77	1

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

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	2364	5808.19	6102.77	2364	0	2364	15	5195	15	0
Yices2	0	2356	7052.42	7346.76	2356	0	2356	23	5195	23	0
Z3-Owl	0	2329 (base +13)	11196.05	11490.87	2329	0	2329	50	5195	48	2
cvc5	0	2294	13439.39	13725.41	2294	0	2294	85	5195	85	0
SMTInterpol	0	1937	73258.20	65529.57	1937	0	1937	442	5195	432	0
Z3-Owl-base ⁿ	0	2316	12169.14	12456.73	2316	0	2316	63	5195	63	0

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

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	7516	4552.41	5485.64	7516	5175	2341	0	58	0	0
Yices2	0	7483	2186.63	3117.64	7483	5161	2322	0	91	0	0
Z3-Owl	0	7360 (base +69)	9317.03	10246.01	7360	5069	2291	0	214	0	0
cvc5	0	6883	8236.43	9087.41	6883	4650	2233	0	691	0	0
SMTInterpol	0	4551	15910.73	7307.31	4551	2835	1716	30	2993	0	0
Z3-Owl-base ⁿ	0	7291	3675.07	4574.71	7291	5019	2272	0	283	0	0

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