Fix slicing bug related to Evaluate Query

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

@@ -6,6 +6,8 @@
 import java.util.Collection;
 import java.util.Iterator;
 
+import org.key_project.util.EqualsModProofIrrelevancy;
+import org.key_project.util.EqualsModProofIrrelevancyUtil;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
@@ -18,7 +20,7 @@
  * future versions it can be enhanced to do other simplifications. A sequent and so a semisequent
  * has to be immutable.
  */
-public class Semisequent implements Iterable<SequentFormula> {
+public class Semisequent implements Iterable<SequentFormula>, EqualsModProofIrrelevancy {
 
     /** the empty semisequent (using singleton pattern) */
     public static final Semisequent EMPTY_SEMISEQUENT = new Empty();
@@ -459,12 +461,25 @@ public boolean equals(Object o) {
         return seqList.equals(((Semisequent) o).seqList);
     }
 
+    @Override
+    public boolean equalsModProofIrrelevancy(Object o) {
+        if (!(o instanceof Semisequent)) {
+            return false;
+        }
+        return EqualsModProofIrrelevancyUtil.compareImmutableLists(seqList,
+            ((Semisequent) o).seqList);
+    }
+
 
     @Override
     public int hashCode() {
         return seqList.hashCode();
     }
 
+    @Override
+    public int hashCodeModProofIrrelevancy() {
+        return EqualsModProofIrrelevancyUtil.hashCodeImmutableList(seqList);
+    }
 
     /** @return String representation of this Semisequent */
     @Override

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

@@ -11,6 +11,7 @@
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
 
 import org.key_project.logic.Name;
+import org.key_project.util.EqualsModProofIrrelevancy;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
@@ -23,7 +24,7 @@
  * {@link Sequent#createSuccSequent} or by inserting formulas directly into
  * {@link Sequent#EMPTY_SEQUENT}.
  */
-public class Sequent implements Iterable<SequentFormula> {
+public class Sequent implements Iterable<SequentFormula>, EqualsModProofIrrelevancy {
 
     public static final Sequent EMPTY_SEQUENT = NILSequent.INSTANCE;
 
@@ -283,6 +284,24 @@ public boolean equals(Object o) {
         return antecedent.equals(o1.antecedent) && succedent.equals(o1.succedent);
     }
 
+    @Override
+    public boolean equalsModProofIrrelevancy(Object o) {
+        if (this == o) {
+            return true;
+        }
+        if (!(o instanceof Sequent o1)) {
+            return false;
+        }
+
+        return antecedent.equalsModProofIrrelevancy(o1.antecedent)
+                && succedent.equalsModProofIrrelevancy(o1.succedent);
+    }
+
+    @Override
+    public int hashCodeModProofIrrelevancy() {
+        return 0;
+    }
+
     /**
      * Computes the position of the given sequent formula on the proof sequent, starting with one
      * for the very first sequent formula.

key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java

@@ -226,8 +226,8 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
 
         final String tacletName = originalStep.getAppliedRuleApp().rule().name().toString();
         TacletApp originalTacletApp = null;
-        if (originalStep.getAppliedRuleApp() instanceof TacletApp) {
-            originalTacletApp = (TacletApp) originalStep.getAppliedRuleApp();
+        if (originalStep.getAppliedRuleApp() instanceof TacletApp tacletApp) {
+            originalTacletApp = tacletApp;
         }
 
         TacletApp ourApp = null;
@@ -238,7 +238,7 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
         if (t == null) {
             // find the correct taclet
             for (NoPosTacletApp partialApp : currGoal.indexOfTaclets()
-                    .getPartialInstantiatedApps()) {
+                    .allNoPosTacletApps()) {
                 if (partialApp.equalsModProofIrrelevancy(originalTacletApp)) {
                     ourApp = partialApp;
                     break;
@@ -249,7 +249,8 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
             }
             if (ourApp == null) {
                 throw new IllegalStateException(
-                    "proof replayer failed to find dynamically added taclet");
+                    "proof replayer failed to find dynamically added taclet at original node "
+                        + originalStep.serialNr());
             }
         } else {
             ourApp = NoPosTacletApp.createNoPosTacletApp(t);

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

@@ -24,6 +24,7 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.Named;
 import org.key_project.util.EqualsModProofIrrelevancy;
+import org.key_project.util.EqualsModProofIrrelevancyUtil;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableMap;
@@ -508,7 +509,7 @@ public boolean equalsModProofIrrelevancy(Object o) {
             return false;
         }
 
-        if (!goalTemplates.equals(t2.goalTemplates)) {
+        if (!EqualsModProofIrrelevancyUtil.compareImmutableLists(goalTemplates, t2.goalTemplates)) {
             return false;
         }
 

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java

@@ -80,6 +80,15 @@ public boolean equals(Object o) {
         return replacewith.equals(other.replacewith);
     }
 
+    @Override
+    public boolean equalsModProofIrrelevancy(Object obj) {
+        if (!super.equalsModProofIrrelevancy(obj)
+                || !(obj instanceof AntecSuccTacletGoalTemplate other)) {
+            return false;
+        }
+        return replacewith.equalsModProofIrrelevancy(other.replacewith);
+    }
+
     @Override
     public int hashCode() {
         int result = 17;

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletGoalTemplate.java

@@ -89,6 +89,15 @@ public boolean equals(Object o) {
         return replacewith.equals(other.replacewith);
     }
 
+    @Override
+    public boolean equalsModProofIrrelevancy(Object obj) {
+        if (!(obj instanceof RewriteTacletGoalTemplate other)
+                || !super.equalsModProofIrrelevancy(obj)) {
+            return false;
+        }
+        return replacewith.equalsModProofIrrelevancy(other.replacewith);
+    }
+
     @Override
     public int hashCode() {
         int result = 17;

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java

@@ -9,6 +9,8 @@
 import de.uka.ilkd.key.logic.op.SchemaVariable;
 import de.uka.ilkd.key.rule.Taclet;
 
+import org.key_project.util.EqualsModProofIrrelevancy;
+import org.key_project.util.EqualsModProofIrrelevancyUtil;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
@@ -19,7 +21,7 @@
  * sequents that have to be added, new rules and rule variables. The replacewith-goal is implemented
  * in subclasses
  */
-public class TacletGoalTemplate {
+public class TacletGoalTemplate implements EqualsModProofIrrelevancy {
 
     /** stores sequent that is one of the new goals */
     private Sequent addedSeq = Sequent.EMPTY_SEQUENT;
@@ -175,4 +177,18 @@ public String toString() {
         }
         return result;
     }
+
+    @Override
+    public boolean equalsModProofIrrelevancy(Object obj) {
+        if (!(obj instanceof TacletGoalTemplate other)) {
+            return false;
+        }
+        return addedSeq.equalsModProofIrrelevancy(other.addedSeq) && EqualsModProofIrrelevancyUtil
+                .compareImmutableLists(addedRules, other.addedRules);
+    }
+
+    @Override
+    public int hashCodeModProofIrrelevancy() {
+        return 0;
+    }
 }