Dependency Contract: Ignore all term labels when searching for base term (#3776)

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java

@@ -96,7 +96,8 @@ public interface SourceElement extends SyntaxElement, EqualsModProperty<SourceEl
      * These are not syntactical equal, therefore false is returned.
      */
     @Override
-    default <V> boolean equalsModProperty(Object o, Property<SourceElement> property, V... v) {
+    default <V> boolean equalsModProperty(Object o, Property<? super SourceElement> property,
+            V... v) {
         if (!(o instanceof SourceElement)) {
             return false;
         }

key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java

@@ -349,7 +349,7 @@ protected int computeHashCode() {
     }
 
     @Override
-    public <V> boolean equalsModProperty(Object o, Property<JTerm> property, V... v) {
+    public <V> boolean equalsModProperty(Object o, Property<? super JTerm> property, V... v) {
         if (!(o instanceof JTerm other)) {
             return false;
         }

key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualsModProperty.java

@@ -49,7 +49,7 @@ public interface EqualsModProperty<T> {
      * @param <V> the type of the additional parameters needed by {@code property} for the
      *        comparison
      */
-    <V> boolean equalsModProperty(Object o, Property<T> property, V... v);
+    <V> boolean equalsModProperty(Object o, Property<? super T> property, V... v);
 
     /**
      * Computes the hash code according to the given ignored {@code property}.

key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java

@@ -41,7 +41,7 @@
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 
-import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY;
+import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY;
 
 
 public final class UseDependencyContractRule implements BuiltInRule, ComplexJustificationable {
@@ -226,7 +226,7 @@ public static boolean isBaseOcc(JTerm focus, JTerm candidate) {
             return false;
         }
         for (int i = 1, n = candidate.arity(); i < n; i++) {
-            if (!(candidate.sub(i).equalsModProperty(focus.sub(i), IRRELEVANT_TERM_LABELS_PROPERTY)
+            if (!(candidate.sub(i).equalsModProperty(focus.sub(i), TERM_LABELS_PROPERTY)
                     || candidate.sub(i).op() instanceof LogicVariable)) {
                 return false;
             }