Alternative for #3393: Fix slicing bug related to Evaluate Query

[WolframPfeifer]

This PR brings the fixes from #3393 to current main by manually transferring the changes. This was necessary since in the meantime, equality modulo proofs is implemented completely differently.

Since a lot of time has passed, I can also provide the problematic example now (was from a student exercise):

• Java class: VarDecl.java
• Proof (remove .txt file ending): VarDecl(VarDecl__add(int)).JML normal_behavior operation contract.0.proof.txt

The proof was not sliceable on main (exception: "proof replayer failed to find dynamically added taclet"), but is with the changes from this PR.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: Manually with the given example

Additional information and contact(s)

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