Skip to content

Fix naming and renaming issues#3804

Merged
unp1 merged 4 commits intomainfrom
fixMergeRuleRenaming
Apr 17, 2026
Merged

Fix naming and renaming issues#3804
unp1 merged 4 commits intomainfrom
fixMergeRuleRenaming

Conversation

@unp1
Copy link
Copy Markdown
Member

@unp1 unp1 commented Apr 14, 2026

Intended Change

Renaming should work more reliably now for:

  • naming conflicts when merging proof branches
  • Newly introduced names for skolemsymbols and program variables should be checked correctly for uniqueness in the current namespace set.

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I have tested the feature as follows: unit tests and a case study I am working on at the moment

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@unp1 unp1 force-pushed the fixMergeRuleRenaming branch 2 times, most recently from 6caceed to 9d63990 Compare April 14, 2026 11:25
@unp1 unp1 added this to the v3.0.0 milestone Apr 17, 2026
@unp1 unp1 added the 🐞 Bug label Apr 17, 2026
unp1 added 4 commits April 17, 2026 12:21
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.
@unp1 unp1 force-pushed the fixMergeRuleRenaming branch from 9d63990 to 561b3d4 Compare April 17, 2026 10:21
@unp1 unp1 added this pull request to the merge queue Apr 17, 2026
Merged via the queue into main with commit db52a54 Apr 17, 2026
36 checks passed
@unp1 unp1 deleted the fixMergeRuleRenaming branch April 17, 2026 11:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants