Predicate AllocationSizeOverflow::additionalStep

Holds if the value of pred can flow into succ in one step, either through a call to len or through an arithmetic operation (other than remainder).