Description

I think this bug is interesting enough to merit an issue. Fix is ready.

The proof replayer does not properly check whether a taclet is actually applicable at the given position. For example, a SuccTaclet like ifElseSplit should only be applied at the top level, but this is not checked at all. Therefore, KeY will accept a proof for the following problem:

   x = 0
-> \<{
     x = 1;
     if (false) {}
     else {}
   }\> x = 0

We use ifElseSplit below the modality, thereby dropping the update to x.

Reproducible

Is the issue reproducible?
Select one of: always, sometimes, random, have not tried, n/a

Always.

Steps to reproduce

Describe the steps needed to reproduce the issue.

1. Unzip the attached file
2. Load the unzipped proof file

if.key.zip

What is your expected behavior and what was the actual behavior?

Expected: Proof is rejected.
Actual: KeY accepts the proof; formula is shown as proven correct.

• Commit: 012874a