anonHeapFunction label prevents use of Dependency Contract #3760

Description

When applying a dependency contract (via "Use Dependency Contract"), KeY considers the labels on the sub-terms in the focus term.
For "proof relevant" labels these have to be present on both the occurence with a smaller heap and the focus term.
But it is fairly easy to get in a situation where the labels differ, and this difference is not really shown to the user.

Reproducible

always

Steps to reproduce

Load the below file, choose AnonHeapLabel::useDependencyContract

import java.util.*;

public class AnonHeapLabel {
    /*@ accessible \nothing;
      @ helper model static public boolean hasArc(Object obj) {
          return true;
        }
      @*/

    /*@ public normal_behavior
      @ requires (\forall \bigint i; 0 <= i && i < list.seq.length; list.seq[i] instanceof Object && (Object)list.seq[i] != null);
      @ ensures hasArc((Object)list.seq[0]);
      @*/
    static void useDependencyContract(List list) {
        /*@ loop_invariant hasArc((Object)list.seq[0]);
          @ decreases 5 - i;
          @ assignable list.seq;
          @*/
        for (int i = 0; i < 5; i++) {
            
        }
        otherMethod(new ArrayList());
    }

    /*@ public normal_behavior
      @ ensures true;
      @ assignable param.seq;
      @*/
    static void otherMethod(List param) {
    
    }
}

1. Run symbolic execution macro
2. Navigate to proof goal below "Post (otherMethod)"
3. Run OSS on last formula
4. Perform eqTermCut on list.seq@heapAfter_otherMethod (in last formula) with inst. list.seq@anon_heap_LOOP_0
5. Perform applyEq on list.seq@heapAfter_otherMethod (in last formula)
6. Try to Use Dependency Contract on AnonHeapLabel.hasArc(...) in last formula
7. Perform eqTermCut on list.seq@anon_heap_LOOP_0 (in first formula) with inst. list.seq@anon_heap_LOOP_0 (yes, exactly the same formula)
8. Perform applyEq on list.seq@anon_heap_LOOP_0 (in first formula)
9. Try to Use Dependency Contract again

Expected behavior: Step 6 already works
Actual behavior: only Step 9 works

Additional information

I have a potential fix but I'm not sure it wouldn't break other stuff:

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java
index 596410ce3e..e85501bea4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java
@@ -154,6 +154,11 @@ public final class ParameterlessTermLabel implements TermLabel {
         return 0;
     }
 
+    @Override
+    public boolean isProofRelevant() {
+        return name != ANON_HEAP_LABEL_NAME;
+    }
+
     @Override
     public String toString() {
         return name.toString();

• Commit: