Description
The widening API requires that analyses return the previous value when it is equivalent to the current values's widening. But, that equivalence is with respect to the previous environment (and its flow condition), while the widening operation will save the current environment. So, when checking equivalence, the operation succeeds, but then the resulting environment is incoherent -- the previous value is saved with the current flow condition. It is easy to trigger situations where the current flow condition is too weak to prove assertions about the previous value (for example, that a given property is false).
Any given implementation of widening can address this issue by adding any needed assumptions to the current environment. But, seems more like a forced workaround than a proper solution. It seems better to modify the API to allow implementations to independently return the desired widened value and the indication of whether or not it is identical to the previous value.