When the user adds an equivalence condition to handle an observable difference, the introduced condition is not put into the assumption context until the next time that node is processed. The result is that subsequent widening steps will occur in the weakened assumption context (i.e. not assuming the equivalence condition) and the result is a weaker equivalence domain than we would expect.
All of the call sites for observable checks (only 3 or so) need to be modified to handle the case where the node processing is to be immediately stopped and re-started with the additional assumption in scope, to avoid introducing this weakened equivalence condition and propagating it forward.
An alternative approach would be to queue the modification to occur after the node processing is finished (which will then cause that node to be immediately re-queued). This does a little bit of redundant work (i.e. any work done after the observable difference is found needs to be re-done), but probably involves changing less code.
When the user adds an equivalence condition to handle an observable difference, the introduced condition is not put into the assumption context until the next time that node is processed. The result is that subsequent widening steps will occur in the weakened assumption context (i.e. not assuming the equivalence condition) and the result is a weaker equivalence domain than we would expect.
All of the call sites for observable checks (only 3 or so) need to be modified to handle the case where the node processing is to be immediately stopped and re-started with the additional assumption in scope, to avoid introducing this weakened equivalence condition and propagating it forward.
An alternative approach would be to queue the modification to occur after the node processing is finished (which will then cause that node to be immediately re-queued). This does a little bit of redundant work (i.e. any work done after the observable difference is found needs to be re-done), but probably involves changing less code.