fn estimate_inbound_witness(
root_closure: &FxHashSet<Local>,
numeric_summary: &LoopNumericSummary,
) -> Option<usize>Expand description
Estimate an index-range witness for InBound.
The current implementation recognizes that a checked pointer/index depends
on an induction variable. It returns the first loop-body count that is not
covered by --postfix-repeat 1; a later affine summary can replace this
fallback with a symbolic i in [0, len) proof and a concrete witness.