Fix broken proof tree after information flow auto pilot#3911
Merged
Conversation
The Full Information Flow Auto Pilot broke the proof tree view with
'IllegalStateException: abstract tree node without parent: Proof Tree'.
Root cause: when the macro creates its auxiliary side proof, the
StartSideProofMacro handling in macroFinished re-froze the interface via
initiateAutoMode(sideProof), which also broadcasts autoModeStarted for
the side proof (with no matching autoModeStopped ever following). The
ProofTreeView listener trusted any event source and overwrote its
modifiedSubtrees bookkeeping with the side proof's goal nodes. At the
final autoModeStopped, those foreign (by then disposed) nodes were fed
into the tree model of the displayed proof, where the lazily created
parent branch node for the foreign root has no parent and a disposed
proof has no root() anymore, defeating the existing root check.
The fix prevents the poisoning at both ends:
- macroFinished only freezes the interface (stopInterface +
setInteractive) instead of broadcasting a spurious autoModeStarted
for the side proof,
- ProofTreeView ignores auto mode events for proofs it does not display
and skips foreign nodes when refreshing modified subtrees.
GUIAbstractTreeNode.getParent() keeps failing fast on parent-less
nodes so that bookkeeping bugs of this kind surface; the previously
unexplained root-instance escape ('why can there be another instance
of the root node?') is now documented - it stems from stale instances
after cache invalidation and from exactly this kind of foreign-node
walk. A regression test pins the fail-fast contract.
Created with AI tooling
wadoon
approved these changes
Jul 10, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Related Issue
This pull request resolves #3713.
Intended Change
Applying the Full Information Flow Auto Pilot destroyed the proof tree view with
The root problem was that two autoModeStarted events were fired, one for the main proof and
one for the side proof. The side proof finished sent its autoModeStopped and the GUI tree
was informed about node changes of the tree it did not show and as the side proof was disposed
an NPE was triggered.
The actual fix is in
AbstractMediatorUserInterfaceControl.macroFinished. The ProofTreeViewhas a robustness fix discarding any information about a proof it does not display. The error is
not silenced as we still get an Exception from GUIAbstractTreeNode, but that is more fail fast and
once, while the other exception from ProofTreeView would render the whole GUI unresponsive.
AbstractMediatorUserInterfaceControl.macroFinishedonly freezes the interface(
stopInterface+setInteractive(false)) instead of broadcasting a spuriousautoModeStartedfor the side proof.ProofTreeViewignores auto mode events for proofs it does not display, and skips foreignnodes when refreshing modified subtrees in
autoModeStopped.DisposedProofTreeUpdateTestreproduces the #3713 constellation headlessly (a foreign disposedproof's node fed into a live proof's model) and pins the fail-fast contract.
Verified interactively: the auto pilot no longer breaks the proof tree.
Note: while verifying the fix another issue showed up, namely that information flow proofs additionally do not close interactively, an independent regression of the problem loader's profile handling, fixed in a separate follow-up PR.
Type of pull request
Ensuring quality
DisposedProofTreeUpdateTest),manual GUI verification with the InformationFlow examples (the exact reproduction steps of
Macro
auto-infflowbreaks UI Proof Tree #3713).Additional information and contact(s)
PR created with AI tooling
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.