It would be more flexible for a compiler to reuse the range analysis logic used in optimizations for statically verifiable divide by zeros. That way you could extend it to other things like statically verifiable overflows.