Use Dependency Contract does not work for heap like `heap[create(h_2)][h_2.<initialized> := TRUE]`

[FliegendeWurst]

Description

Use Dependency Contract doesn't apply successfully if the (larger) heap looks like heap[create(h_2)][h_2.<initialized> := TRUE].
No window is opened (to select a heap) and no proof node is created.

Reproducible

always

Steps to reproduce

1. Clone https://github.com/FliegendeWurst/Jerboa-KeY-case-study/tree/wip-2 (wip-2 branch)
2. Open verifDuplicateNodeGraph.proof.gz
3. Navigate to open goal with node ID 562
4. Try to apply "Use Dependency Contract" on graph.nodes.<inv>@heap[create(h_2)][h_2.<initialized> := TRUE]

Expected behavior: it works
Actual behavior: it doesn't work, with no error message or stack trace

Additional information

---

• Commit: 2a56855

[WolframPfeifer]

Is it possible to provide a more stripped down example? This here is quite laborious to reproduce ...

A common mistake/misconception is the following: In the formula from above, the nested select graph.nodes is also evaluated on the larger heap (heap[create(h_2)][h_2.<initialized> := TRUE]), while the formula in the antecedent is actually completely evaluated on the smaller heap:

graph.nodes.<inv>@heap
==>
graph.nodes.<inv>@heap[create(h_2)][h_2.<initialized> := TRUE]

You can apply simplification rules like selectOfStore, selectOfCreate etc. on graph.nodes to achieve the following sequent:

graph.nodes.<inv>@heap
==>
(graph.nodes@heap).<inv>@heap[create(h_2)][h_2.<initialized> := TRUE]

Here, the dependency contract should be applicable.