Fix slicing bug related to Evaluate Query

FliegendeWurst commented 8 months ago

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.

codecov[bot] commented 8 months ago

Codecov Report

Attention: Patch coverage is 3.44828% with 28 lines in your changes are missing coverage. Please review.

Project coverage is 37.84%. Comparing base (99658cc) to head (d19e2d7). Report is 3 commits behind head on main.

:exclamation: Current head d19e2d7 differs from pull request most recent head a0746d8

Please upload reports for the commit a0746d8 to get more accurate results.

Files	Patch %	Lines
...e/src/main/java/de/uka/ilkd/key/logic/Sequent.java	0.00%	7 Missing :warning:
...lkd/key/rule/tacletbuilder/TacletGoalTemplate.java	0.00%	5 Missing :warning:
...c/main/java/de/uka/ilkd/key/logic/Semisequent.java	0.00%	4 Missing :warning:
...ule/tacletbuilder/AntecSuccTacletGoalTemplate.java	0.00%	4 Missing :warning:
.../rule/tacletbuilder/RewriteTacletGoalTemplate.java	0.00%	4 Missing :warning:
...a/ilkd/key/proof/replay/AbstractProofReplayer.java	25.00%	2 Missing and 1 partial :warning:
...ore/src/main/java/de/uka/ilkd/key/rule/Taclet.java	0.00%	1 Missing :warning:

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3393 +/- ## ============================================ - Coverage 38.02% 37.84% -0.19% + Complexity 17080 17042 -38 ============================================ Files 2099 2082 -17 Lines 127189 127315 +126 Branches 21368 21447 +79 ============================================ - Hits 48369 48183 -186 - Misses 72856 73219 +363 + Partials 5964 5913 -51 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

WolframPfeifer commented 7 months ago

This PR fixes one of the original bug (file belongs to a student exercise, thus I do not want to attach it for the moment). However, there is a follow-up bug with the same file. Could you also look into the second bug, please?

FliegendeWurst commented 7 months ago

I think the other bug you are referring to is fixed by #3438

WolframPfeifer commented 7 months ago

I think the other bug you are referring to is fixed by #3438

Yes, thanks. I did not notice the other fix.

FliegendeWurst commented 7 months ago

I really don't understand the test failure. None of the changes in this PR change anything relevant to normal proof search. I'll do a no-op commit and push again.

tobias-rnh commented 6 months ago

I really don't understand the test failure. None of the changes in this PR change anything relevant to normal proof search. I'll do a no-op commit and push again.

I was having trouble with tests failing for no reason at all in the last few weeks too. First it was the unit tests only on Ubuntu and then the integration test testRunAllFunProofs. The caches in the repository were completely filled and after making some space, we got the tests to pass. I don't know if this could also be the problem here, but it might be worth a try.

KeYProject / key