From fd9c1f4f0e946a6e703b26fbb0ceba380c5b67f7 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 14 Apr 2026 12:50:58 +0200 Subject: [PATCH 1/4] Fix name collision resolution in merge rule Name collisions when merging can also appear for different op kinds, e.g. a program variable named i_1 and a skolem function named i_1. Until know this resulted in a CastException as the assumption was that conflicts happen only between program variables or only between function symbols. --- .../key/util/mergerule/MergeRuleUtils.java | 59 +++++++++++-------- 1 file changed, 34 insertions(+), 25 deletions(-) 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 From 9812b23fc01dc9471b4d6ca36c40ca078df076de Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 14 Apr 2026 12:52:38 +0200 Subject: [PATCH 2/4] Fix renaming check --- .../main/java/de/uka/ilkd/key/proof/VariableNameProposer.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; From 85650794a27df7e9d72a19967c539139b4d74c3c Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 14 Apr 2026 12:53:23 +0200 Subject: [PATCH 3/4] Ensure that new name generated due to a conflict with a previous proposal is checked for uniqueness --- .../main/java/de/uka/ilkd/key/logic/VariableNamer.java | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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; } From 561b3d422ec35a6b6aaeca14b1bf4ddf863b043b Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 14 Apr 2026 13:21:31 +0200 Subject: [PATCH 4/4] Fix proof script --- key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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);