BaseInvariant internal computations can overflow

[sim642]

We have AnalysisState.executing_speculative_computations disabled in BaseInvariant, so overflow warnings are not produced from these computations, but that's not the whole story. With sem.int.signed_overflow being assume_top, it can still lead to imprecise results.

For example consider x + 1 <= 100 with intervals:

1. BaseInvariant uses the inequality and its right argument to refine the left argument with ID.ending 100 = [min_int, 100].
2. BaseInvariant then uses that value and the right argument of the addition to compute the refined left argument of the addition using ID.sub [min_int,100] [1,1] = [min_int-1,99].
3. If sem.int.signed_overflow is assume_top/assume_wraparound, then this ID.sub handles the underflow and returns top ([min_int,max_int]) instead.

Thus x cannot be refined at all. And this is even when the program itself has no overflow in x + 1 because it may be bounded, e.g. x = [min_int,1000].
The overflow in BaseInvariant doing the subtraction (or whatever other operation) to do the backward evaluation is purely caused by itself: the way inequalities are refined by ID.ending constructs the interval with min_int lower bound (the program cannot refine this in any way) and performs ID.sub on that.

So just suppressing overflow warnings in BaseInvariant isn't enough. Instead its (speculative) computations should assume no overflows also in the values the domains compute. Although I have no idea if temporarily changing the option to assume_none is the right thing.