QF_FP (Model Validation Track)

Competition results for the QF_FP logic in the Model Validation Track. Chart

Results were generated on 2026-07-25

Benchmarks: 2416
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 SAT	Unsolved	Timeout
Bitwuzla	2416	1862.42	2164.01	2416	2416	0	0
cvc5	2416	3106.31	3407.77	2416	2416	0	0
z3-BooledASS ^ne	2302 (base -91)	401.45	684.22	2302	2302	114	9
z3-BooledASS-base ⁿ	2393	519.22	813.31	2393	2393	23	7

(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 SAT	Unsolved	Timeout
Bitwuzla	2416	1862.42	2164.01	2416	2416	0	0
cvc5	2416	3106.31	3407.77	2416	2416	0	0
z3-BooledASS ^ne	2302 (base -91)	401.45	684.22	2302	2302	114	9
z3-BooledASS-base ⁿ	2393	519.22	813.31	2393	2393	23	7

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Bitwuzla	2416	1862.42	2164.01	2416	2416	0	0
cvc5	2416	3106.31	3407.77	2416	2416	0	0
z3-BooledASS ^ne	2302 (base -91)	401.45	684.22	2302	2302	114	9
z3-BooledASS-base ⁿ	2393	519.22	813.31	2393	2393	23	7

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
Bitwuzla	2406	415.71	715.69	2406	2406	0	10
cvc5	2406	460.16	760.08	2406	2406	0	10
z3-BooledASS ^ne	2302 (base -89)	401.45	684.22	2302	2302	96	18
z3-BooledASS-base ⁿ	2391	419.50	713.33	2391	2391	9	16

SMT-COMP 2026