SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_UFBV (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 764
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	SMTInterpol	SMTInterpol

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	659	16970.39	17055.21	659	200	459	105	0	104	1
Yices2	0	623	55409.17	55494.10	623	200	423	141	0	141	0
SMTInterpol	0	595	21253.20	12627.67	595	84	511	169	0	42	0
cvc5	0	583	195891.80	195998.87	583	165	418	181	0	111	70
Z3-Owl	0	528 (base +140)	59892.03	59966.62	528	153	375	236	0	192	20
Z3-Owl-base ⁿ	0	388	47740.49	47794.89	388	145	243	376	0	376	0

(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	659	16970.39	17055.21	659	200	459	105	0	104	1
Yices2	0	623	55409.17	55494.10	623	200	423	141	0	141	0
SMTInterpol	0	595	21253.20	12627.67	595	84	511	169	0	42	0
cvc5	0	583	195891.80	195998.87	583	165	418	181	0	111	70
Z3-Owl	0	528 (base +140)	59892.03	59966.62	528	153	375	236	0	192	20
Z3-Owl-base ⁿ	0	388	47740.49	47794.89	388	145	243	376	0	376	0

(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	200	8407.60	8434.04	200	200	0	2	562	1	1
Yices2	0	200	22621.40	22649.51	200	200	0	2	562	2	0
cvc5	0	165	34710.63	34736.81	165	165	0	37	562	5	32
Z3-Owl	0	153 (base +8)	7873.82	7894.49	153	153	0	49	562	40	1
SMTInterpol	0	84	5886.75	4637.65	84	84	0	118	562	25	0
Z3-Owl-base ⁿ	0	145	21865.19	21885.83	145	145	0	57	562	57	0

(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
SMTInterpol	0	511	15366.45	7990.01	511	0	511	4	249	4	0
Bitwuzla	0	459	8562.80	8621.17	459	0	459	56	249	56	0
Yices2	0	423	32787.77	32844.59	423	0	423	92	249	92	0
cvc5	0	418	161181.17	161262.06	418	0	418	97	249	76	21
Z3-Owl	0	375 (base +132)	52018.21	52072.13	375	0	375	140	249	111	15
Z3-Owl-base ⁿ	0	243	25875.30	25909.07	243	0	243	272	249	272	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
SMTInterpol	0	529	12103.55	5029.45	529	64	465	93	142	0	0
Bitwuzla	0	521	5163.91	5229.33	521	94	427	0	243	0	0
Yices2	0	342	3301.40	3344.29	342	110	232	0	422	0	0
Z3-Owl	0	307 (base +216)	2552.57	2591.73	307	119	188	0	457	0	0
cvc5	0	29	473.70	477.40	29	25	4	0	735	0	0
Z3-Owl-base ⁿ	0	91	881.70	893.02	91	68	23	0	673	0	0

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