We can sharpen the range of a AddRec if we know that it does not
self-wrap and know the symbolic iteration count in the loop. If we can
evaluate the value of AddRec on the last iteration and prove that at least
one its intermediate value lies between start and end, then no-wrap flag
allows us to conclude that all of them also lie between start and end. So
the estimate of range can be improved to union of ranges of start and end.
Switched off by default, can be turned on by flag.
I'm concerned that evaluating at iteration MaxBECount won't do what you want. In particular, if MaxBECount is larger than the number of steps required to violate nw, then the way you're comparing Start and End doesn't work.
The actual backedge-taken count at runtime can't be that large, of course, but MaxBECount is an approximation in general; I don't think we make any relevant guarantees. In particular, if the step isn't constant, we can't get this right.
I think you could explicitly compute the largest number of non-wrapping iterations, and then take the minimum of that and MaxBECount to compute the "real" maximum count.