-
Notifications
You must be signed in to change notification settings - Fork 41
Open
Milestone
Description
Description
Loading an information flow proof obligation, and applying the auto-infflow macro results into a destroyed Proof Tree in the JTree, and a stack trace. UI is not usable anymore.
Exception in thread "AWT-EventQueue-0" java.lang.IllegalStateException: abstract tree node without parent: Proof Tree
at de.uka.ilkd.key.gui.prooftree.GUIAbstractTreeNode.getParent(GUIAbstractTreeNode.java:49)
at de.uka.ilkd.key.gui.prooftree.GUIAbstractTreeNode.getPath(GUIAbstractTreeNode.java:82)
at de.uka.ilkd.key.gui.prooftree.GUIProofTreeModel.updateTree(GUIProofTreeModel.java:413)
at de.uka.ilkd.key.gui.prooftree.GUIProofTreeModel.updateTree(GUIProofTreeModel.java:421)
at de.uka.ilkd.key.gui.prooftree.ProofTreeView$GUIProofTreeProofListener.autoModeStopped(ProofTreeView.java:957)
at de.uka.ilkd.key.control.AbstractProofControl.fireAutoModeStopped(AbstractProofControl.java:563)
at de.uka.ilkd.key.ui.MediatorProofControl.fireAutoModeStopped(MediatorProofControl.java:73)
at de.uka.ilkd.key.gui.ProofMacroWorker.done(ProofMacroWorker.java:133)
Reproducible
Is the issue reproducible?
always
Steps to reproduce
- Load infflow PO from the examples dialog.
- Apply the "Full Information Flow Auto Pilot"
- Wait...
- Be happy about the broken proof tree:

What is your expected behavior and what was the actual behavior?
Closed proof with a valid proof tree
Additional information
Bug is on main. Introduction unknown.