The bound is ∑r=1..k|Δ|r. Reachable counts the guard-satisfiable blocks actually enumerated; merged applies canonical merging. Reachable grows about linearly in k, not exponentially.