SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_BVFP (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 527
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	527	558.10	622.80	527	238	289	0	0	0	0
cvc5	0	527	3213.56	3278.46	527	238	289	0	0	0	0
Z3-Owl	0	510 (base +9)	10278.54	10344.55	510	230	280	17	0	10	5
COLIBRI	0	462	385.91	442.71	462	228	234	65	0	21	0
colibri2	0	382	1915.19	1962.08	382	167	215	145	0	19	0
Z3-Owl-base ⁿ	0	501	18398.34	18462.61	501	228	273	26	0	21	3

(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	527	558.10	622.80	527	238	289	0	0	0	0
cvc5	0	527	3213.56	3278.46	527	238	289	0	0	0	0
Z3-Owl	0	510 (base +9)	10278.54	10344.55	510	230	280	17	0	10	5
COLIBRI	0	462	385.91	442.71	462	228	234	65	0	21	0
colibri2	0	382	1915.19	1962.08	382	167	215	145	0	19	0
Z3-Owl-base ⁿ	0	501	18398.34	18462.61	501	228	273	26	0	21	3

(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	238	97.52	126.70	238	238	0	0	289	0	0
cvc5	0	238	1105.79	1135.03	238	238	0	0	289	0	0
Z3-Owl	0	230 (base +2)	2718.39	2747.89	230	230	0	8	289	3	5
COLIBRI	0	228	179.20	207.25	228	228	0	10	289	2	0
colibri2	0	167	657.86	678.33	167	167	0	71	289	7	0
Z3-Owl-base ⁿ	0	228	4606.74	4635.42	228	228	0	10	289	7	3

(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	289	460.58	496.11	289	0	289	0	238	0	0
cvc5	0	289	2107.77	2143.43	289	0	289	0	238	0	0
Z3-Owl	0	280 (base +7)	7560.15	7596.66	280	0	280	9	238	7	0
COLIBRI	0	234	206.71	235.47	234	0	234	55	238	19	0
colibri2	0	215	1257.33	1283.75	215	0	215	74	238	12	0
Z3-Owl-base ⁿ	0	273	13791.60	13827.19	273	0	273	16	238	14	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	523	374.50	438.69	523	238	285	0	4	0	0
cvc5	0	500	998.99	1060.27	500	226	274	0	27	0	0
COLIBRI	0	461	339.99	396.66	461	228	233	44	22	0	0
Z3-Owl	0	416 (base +12)	1988.93	2041.99	416	208	208	0	111	0	0
colibri2	0	375	182.81	228.64	375	165	210	82	70	0	0
Z3-Owl-base ⁿ	0	404	1392.52	1442.36	404	205	199	0	123	0	0

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