Update to LocationVariable is ignored after pruning

[gewitternacht]

Description

Sometimes the simplifyUpdate1/simplifyUpdate2 rules ignore updates, specifically to LoctionVaribales. This seems to be caused by preceding pruning. In my case something like { ... || heapBefore_foo:=heap || ... }heapBefore_foo was "simplified" to heapBefore_foo instead of heap.

Reproducible

always

Steps to reproduce

1. load the foo()-Method from Updates.java into KeY
2. execute Full Auto Pilot→ the proof is closed
3. prune the whole proof tree
4. execute Full Auto Pilot again → the proof is not closed
5. apply One Step Simplification on the remaining goal (Validity of the assertion)
   → the resulting formula contains self.modelMethod()@heapBefore_foo, which should be self.modelMethod() – the update heapBefore_foo:=heap should have been applied, but was ignored
6. save the proof in its current state
7. relaod the previously saved proof and go to the remaining goal
   → now the formula correctly contains self.modelMethod()

Updates.java.zip

---

• Commit: 69fd94726f5bf6c2c5ddd3dec2e2ed80241bc9d7