QF_FP (Unsat Core Track)

Competition results for the QF_FP logic in the Unsat Core Track. Chart

Results were generated on 2026-07-25

Benchmarks: 2406
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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
Bitwuzla	17	1181.96	1482.21	2406	2406	0	0
cvc5	8	583.77	883.78	2406	2406	0	0
z3-BooledASS ^ne	6 (base +0)	18730.97	19029.30	2404	2404	2	2
z3-BooledASS-base ⁿ	6	18803.77	19102.54	2404	2404	2	2

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
Bitwuzla	17	1181.96	1482.21	2406	2406	0	0
cvc5	8	583.77	883.78	2406	2406	0	0
z3-BooledASS ^ne	6 (base +0)	18730.97	19029.30	2404	2404	2	2
z3-BooledASS-base ⁿ	6	18803.77	19102.54	2404	2404	2	2

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
Bitwuzla	17	1181.96	1482.21	2406	2406	0	0
cvc5	8	583.77	883.78	2406	2406	0	0
z3-BooledASS ^ne	6 (base +0)	18730.97	19029.30	2404	2404	2	2
z3-BooledASS-base ⁿ	6	18803.77	19102.54	2404	2404	2	2

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
Bitwuzla	14	802.02	1102.07	2405	2405	1
cvc5	4	400.04	699.91	2405	2405	1
z3-BooledASS ^ne	4 (base +0)	1013.10	1288.42	2235	2235	171
z3-BooledASS-base ⁿ	4	1016.81	1292.74	2235	2235	171

SMT-COMP 2026