key icon indicating copy to clipboard operation
key copied to clipboard

Fix slicing bug related to Evaluate Query

Open FliegendeWurst opened this issue 1 year ago • 6 comments

Intended Change

This PR fixes a slicing failure with a specific proof. In that particular case, the dynamically added taclet was slightly too different for the previous code to pick it up.

Type of pull request

  • [x] Bug fix (non-breaking change which fixes an issue)
  • [ ] Refactoring (behaviour should not change or only minimally change)
  • [ ] New feature (non-breaking change which adds functionality)
  • [ ] Breaking change (fix or feature that would cause existing functionality to change)
  • [x] There are changes to the (Java) code
  • [ ] There are changes to the taclet rule base
  • [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
  • [ ] Other:

Ensuring quality

  • [ ] I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • [ ] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
  • [ ] I added new test case(s) for new functionality.
  • [x] I have tested the feature as follows: slicing now works for the (confidential) proof file
  • [ ] I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

cc @WolframPfeifer who reported the bug

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

FliegendeWurst avatar Jan 31 '24 15:01 FliegendeWurst