Fix naming and renaming issues

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

@@ -382,7 +382,14 @@ protected ProgramElementName getNameProposalForSchemaVariable(String basename,
                         collision = false;
                         for (String previousProposal : previousProposals) {
                             if (previousProposal.equals(result.toString())) {
-                                result = createName(basename, ++cnt, null);
+                                cnt += 1;
+                                result = createName(basename, cnt, null);
+
+                                while (services.getNamespaces().lookupLogicSymbol(result) != null) {
+                                    cnt += 1;
+                                    result = createName(basename, cnt, null);
+                                }
+
                                 collision = true;
                                 break;
                             }

key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java

@@ -138,7 +138,7 @@ private String getNameProposalForSkolemTermVariable(String name, Services servic
             name = basename + cnt;
             l_name = new Name(name);
             cnt++;
-        } while (nss.lookup(l_name) != null && !previousProposals.contains(name));
+        } while (nss.lookup(l_name) != null || previousProposals.contains(name));
 
 
         return name;

key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java

@@ -1182,31 +1182,10 @@ public static Pair<SymbolicExecutionState, SymbolicExecutionState> handleNameCla
 
                 Operator newOp1;
                 Operator newOp2;
-                if (partnerStateOp instanceof Function partnerFun) {
-                    newOp1 = rename(new Name(tb.newName(partnerStateOp.name().toString(),
-                        thisGoal.getLocalNamespaces())), (Function) mergeStateOp);
-                    thisGoalNamespaces.functions().add((Function) newOp1);
-                    thisGoalNamespaces.flushToParent();
-
-                    newOp2 = rename(new Name(tb.newName(partnerStateOp.name().toString(),
-                        thisGoal.getLocalNamespaces())), partnerFun);
-                    thisGoalNamespaces.functions().add((Function) newOp2);
-                    thisGoalNamespaces.flushToParent();
-                } else if (partnerStateOp instanceof LocationVariable partnerLV) {
-                    newOp1 = rename(new Name(tb.newName(partnerStateOp.name().toString(),
-                        thisGoal.getLocalNamespaces())), (LocationVariable) mergeStateOp);
-                    thisGoalNamespaces.programVariables().add((LocationVariable) newOp1);
-                    thisGoalNamespaces.flushToParent();
-
-                    newOp2 = rename(new Name(tb.newName(partnerStateOp.name().toString(),
-                        thisGoal.getLocalNamespaces())), partnerLV);
-                    thisGoalNamespaces.programVariables().add((LocationVariable) newOp2);
-                    thisGoalNamespaces.flushToParent();
-                } else {
-                    throw new RuntimeException(
-                        "MergeRule: Unexpected type of Operator involved in name clash: "
-                            + partnerStateOp.getClass().getSimpleName());
-                }
+
+                newOp1 = renameMergeParticipantOp(partnerStateOp, mergeStateOp, thisGoal);
+
+                newOp2 = renameMergeParticipantOp(partnerStateOp, partnerStateOp, thisGoal);
 
                 mergeState = new SymbolicExecutionState(
                     OpReplacer.replace(mergeStateOp, newOp1, mergeState.getSymbolicState(), tb.tf(),
@@ -1227,6 +1206,36 @@ public static Pair<SymbolicExecutionState, SymbolicExecutionState> handleNameCla
         return new Pair<>(mergeState, mergePartnerState);
     }
 
+    /**
+     * returns an operator of the same kind like <code>mergeStateOp</code> but with a unique name
+     *
+     * @param partnerStateOp the {@link Operator} on whose name the name is based
+     * @param mergeStateOp the {@link Operator} to rename
+     * @param thisGoal the {@link Goal} where the <code>mergeStateOp</code> occurs
+     * @return the renamed {@link Operator}
+     */
+    private static @NonNull Operator renameMergeParticipantOp(Operator partnerStateOp,
+            Operator mergeStateOp, Goal thisGoal) {
+        final TermBuilder tb = thisGoal.getOverlayServices().getTermBuilder();
+        final NamespaceSet thisGoalNamespaces = thisGoal.getLocalNamespaces();
+        Operator newOp1;
+        if (mergeStateOp instanceof Function mergeFct) {
+            newOp1 = rename(new Name(tb.newName(partnerStateOp.name().toString(),
+                thisGoal.getLocalNamespaces())), mergeFct);
+            thisGoalNamespaces.functions().add((Function) newOp1);
+        } else if (mergeStateOp instanceof LocationVariable mergeLV) {
+            newOp1 = rename(new Name(tb.newName(partnerStateOp.name().toString(),
+                thisGoal.getLocalNamespaces())), mergeLV);
+            thisGoalNamespaces.programVariables().add((LocationVariable) newOp1);
+        } else {
+            throw new RuntimeException(
+                "MergeRule: Unexpected type of Operator involved in name clash: " +
+                    mergeStateOp + " : " + mergeStateOp.getClass().getSimpleName());
+        }
+        thisGoalNamespaces.flushToParent();
+        return newOp1;
+    }
+
     /**
      * Parses a declaration of the type "&lt;SORT&gt; &lt;NAME&gt;", where &lt;SORT&gt; must be a
      * sort known to the proof and &lt;NAME&gt; must be a fresh name. This method is used, for

key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof

@@ -385,14 +385,14 @@ instantiate hide var=iv with=(jv_1);
 instantiate hide var=jv with=(v_x_0);
 rule impLeft;
 tryclose branch;
-tryclose branch;
+// tryclose branch;
 // established: r4 is permutation
 // established: r4 fixes v_y_0
 // from now on  v_x_0 != v_y_0 and s_0[v_x_0]!= v_x_0 and
 // s_0[v_y_0]!= v_y_0  and s_0[v_x_0]!= v_y_0 and  s_0[v_y_0]!=v_x_0;
 // this corresponds to case B4iv in the Notes
 // in the following r5 refers to this instantion
-tryclose branch;
+//tryclose branch;
 // established: r5 is of the correct length
 rule seqNPermSwapNPerm formula=(seqNPerm(s_0));
 instantiate hide var=iv with=(v_x_0);