Currently, we check in invariant that the result of casting to the new ik is ID.leq the uncast value.
As we do not do a reduced product, this causes some issues when one of the domain is imprecise:
E.g., because of DefExc, component-wise leq might not hold, even if it still holds for interval domain.
CastE: Lval(Var(i, NoOffset)) evaluates to (Unknown int([-31,31]),[0,2147483647])
which is bigger than the type it is cast to which is unsigned int
This replaced the checks with checks on intervals. This leads to the assertion in the example now passing and no overflow messages being emitted any more
Currently, we check in invariant that the result of casting to the new
ikisID.leqthe uncast value.As we do not do a reduced product, this causes some issues when one of the domain is imprecise: E.g., because of DefExc, component-wise
leqmight not hold, even if it still holds for interval domain.This replaced the checks with checks on intervals. This leads to the assertion in the example now passing and no overflow messages being emitted any more
References #1296