It is not possible to slice the following program when pruning the proof and rerunning automode.
class Newnames {
/*@ normal_behaviour
@ ensures true;
@*/
void createArray() {
int[] a = new int[5 + 1];
}
}
Reproducible
always
Steps to reproduce
Load Newnames.java
Run automode to completion
Prune to node 13
Run automode again
Try to slice the proof
What is your expected behavior and what was the actual behavior?
Expected: slicing works
Actual: failed to find new formula @ variableDeclaration (serial nr 112)
Additional information
Stacktrace:
```
java.lang.IllegalStateException: failed to find new formula @ variableDeclaration (serial nr 112)
at de.uka.ilkd.key.proof.replay.AbstractProofReplayer.constructTacletApp(AbstractProofReplayer.java:263)
at de.uka.ilkd.key.proof.replay.AbstractProofReplayer.reApplyRuleApp(AbstractProofReplayer.java:103)
at org.key_project.slicing.SlicingProofReplayer.slice(SlicingProofReplayer.java:202)
at org.key_project.slicing.ui.SlicingLeftPanel.lambda$sliceProof$8(SlicingLeftPanel.java:447)
at org.key_project.slicing.util.GenericWorker.doInBackground(GenericWorker.java:48)
at org.key_project.slicing.util.GenericWorker.doInBackground(GenericWorker.java:16)
at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:304)
at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:343)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
at java.base/java.lang.Thread.run(Thread.java:833)
```
Description
It is not possible to slice the following program when pruning the proof and rerunning automode.
Reproducible
always
Steps to reproduce
Additional information
Stacktrace: