restart;
a:='a';
a
assume(a>0);
H:=a;
a
subs(a=b, H);
b
a:='a';
a
assume(a>0);
subs(a=b, H);
a
It's clear that last operator return a, not b, because originally H points to "1st assumed a", which is became invalid. How to recalculate ALL "calculated-after-assumptions" expressions to become those pointers valid?