diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java index d128c0f8d6e..bee675efa44 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java +++ b/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; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java index e535726fe3c..c23d9770d32 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java +++ b/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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java index 2b59754e8bc..2fe6a1d92e8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java @@ -1182,31 +1182,10 @@ public static Pair 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 handleNameCla return new Pair<>(mergeState, mergePartnerState); } + /** + * returns an operator of the same kind like mergeStateOp 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 mergeStateOp 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 "<SORT> <NAME>", where <SORT> must be a * sort known to the proof and <NAME> must be a fresh name. This method is used, for diff --git a/key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof b/key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof index bef3d72c971..27d1feea12b 100644 --- a/key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof +++ b/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);