Fix for DepthFirstGoalChooser: Keep enabled sibling goals on a split

[unp1]

Related Issue

Not related to a tracked issue. The bug surfaced while exercising proof caching and is reproducible on main.

Intended Change

Fix automatic proof search stopping with an open goal, and requiring the user to restart it, when proof caching is enabled.

How to reproduce (on current main):

1. Load the example BinarySearch from the examples directory with proof caching on
2. Close it automatically
3. Reload the problem
4. Start the strategies (Full automation)
5. Proof stops at Body Preserves Invariant but should be closed by caching

Reason:
DepthFirstGoalChooser.updateGoalListHelp locates, in its work list, the goal a rule was applied to (the "split point") so it can replace that goal with the rule's new goals. A splitting rule reuses the applied-to goal object for one of its branches (advancing its node), so the split point is found by identity among the new goals rather than by node. That membership test, however, ran against the new goals after they had been filtered to automatic goals. When the reused goal had been disabled — proof caching disables a branch it can close by reference — it was filtered out, the split point was not found, newGoalsInserted stayed false, and the rule's other, still-enabled, new goals were never inserted into the work list. getNextGoal() then eventually returns null while those goals still have applicable rules, so automatic proof search stops with an open goal and the user has to restart it for it to continue.

The fix matches the split point against all new goals (so a disabled reused goal is still found) and inserts only the automatic ones. Behaviour is unchanged when no new goal is disabled, i.e. for all ordinary proof search.

This is a pre-existing bug in DepthFirstGoalChooser, independent of any recent work; it is triggered whenever proof caching disables one branch of a splitting rule.

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 added new test case(s) for new functionality.
• I have tested the feature as follows: added ProofCachingSingleRunTest, which proves a method, then proves a second copy with a reference-search listener that mirrors CachingExtension (disable cache-hit goals during the run, close them afterwards) and asserts the second proof closes in a single automatic run. It fails without the fix (an enabled goal is stranded, requiring a restart) and passes with it. I also verified the multi-core determinism regression test still yields bit-identical proofs (sequential == 4 workers), and that TestReferenceSearcher / TestGoal remain green.
• I have checked that runtime performance has not deteriorated: the change is a no-op whenever no new goal is disabled (the membership set is then identical), so ordinary proof search is byte-identical; only the proof-caching interaction differs.

Additional information and contact(s)

The change is small (three lines of logic plus an explanatory comment) and self-contained in DepthFirstGoalChooser.

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

Created with AI support