SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_FPArith (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_ABVFP : 627 benchmarks
QF_ABVFPLRA : 25 benchmarks
QF_AUFBVFP : 1 benchmarks
QF_BVFP : 527 benchmarks
QF_BVFPLRA : 75 benchmarks
QF_FP : 275 benchmarks
QF_FPLRA : 55 benchmarks
QF_UFFPDTNIRA : 15 benchmarks

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	1561	16627.20	16823.24	1561	603	958	24	15	24	0
cvc5	0	1531	46533.44	46727.92	1531	597	934	69	0	67	2
colibri2	0	1058	13432.45	13563.84	1058	402	656	542	0	148	0
Z3-Owl	0	683 (base +43)	34051.61	34143.10	683	334	349	119	798	66	24
COLIBRI	1	1341	3393.54	3559.28	1342	559	783	243	15	105	0
Z3-Owl-base ⁿ	0	640	45953.98	46038.62	640	310	330	162	798	110	19

(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	1561	16627.20	16823.24	1561	603	958	24	15	24	0
cvc5	0	1531	46533.44	46727.92	1531	597	934	69	0	67	2
colibri2	0	1058	13432.45	13563.84	1058	402	656	542	0	148	0
Z3-Owl	0	683 (base +43)	34051.61	34143.10	683	334	349	119	798	66	24
COLIBRI	1	1341	3393.54	3559.28	1342	559	783	243	15	105	0
Z3-Owl-base ⁿ	0	640	45953.98	46038.62	640	310	330	162	798	110	19

(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	603	8000.21	8076.63	603	603	0	2	995	2	0
cvc5	0	597	11181.41	11256.38	597	597	0	11	992	11	0
colibri2	0	402	5984.54	6034.46	402	402	0	206	992	23	0
Z3-Owl	0	334 (base +24)	16159.74	16204.25	334	334	0	45	1221	12	13
COLIBRI	1	553	893.24	961.65	554	553	1	51	995	23	0
Z3-Owl-base ⁿ	0	310	19910.99	19951.62	310	310	0	69	1221	37	14

(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	958	8626.99	8746.62	958	0	958	8	634	8	0
cvc5	0	934	35352.03	35471.54	934	0	934	44	622	44	0
COLIBRI	0	778	1587.94	1683.93	778	0	778	188	634	78	0
colibri2	0	656	7447.91	7529.38	656	0	656	322	622	121	0
Z3-Owl	0	349 (base +19)	17891.88	17938.85	349	0	349	63	1188	49	5
Z3-Owl-base ⁿ	0	330	26042.99	26086.99	330	0	330	82	1188	68	5

(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	1479	1674.91	1857.02	1479	561	918	0	121	0	0
cvc5	0	1295	3788.88	3947.94	1295	516	779	0	305	0	0
colibri2	0	1004	1055.88	1179.12	1004	382	622	315	281	0	0
Z3-Owl	0	486 (base +37)	2730.63	2792.75	486	244	242	0	1114	0	0
COLIBRI	1	1324	1915.70	2079.14	1325	551	774	138	137	0	0
Z3-Owl-base ⁿ	0	449	1811.51	1866.94	449	235	214	0	1151	0	0

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