What's happening
When SAP shows a popup or error box over the main screen, flowproof currently can't tell "the popup" apart from "the screen behind it" — scene()/surface_text() read every open window flattened together, regardless of which one is actually on top.
If we don't fix it
Tests can report PASS while reading stale or background text, even though the real (topmost) screen shows an error or something different. That's a false-positive pass — the worst class of bug for a testing tool, since it hides real failures instead of catching them. The LLM author can also be offered a target that sits on a window the user can't currently reach.
If we fix it
Tests correctly scope to whichever window (wnd[N]) is actually active, and stop reading content sitting behind an open popup.
Status
Already fixed and tested on PR #467 (active_window/window-scoping logic + GuiMenu filtering, 4 new adapter tests, an 81-step example flow). This issue exists to track the bug independently of that PR, in case it stalls or gets reworked.
Before closing
PR #467 already includes SAP adapter test coverage and a real example flow under examples/sap/ proving the fix — please keep that evidence attached to whichever PR closes this out.
What's happening
When SAP shows a popup or error box over the main screen, flowproof currently can't tell "the popup" apart from "the screen behind it" —
scene()/surface_text()read every open window flattened together, regardless of which one is actually on top.If we don't fix it
Tests can report PASS while reading stale or background text, even though the real (topmost) screen shows an error or something different. That's a false-positive pass — the worst class of bug for a testing tool, since it hides real failures instead of catching them. The LLM author can also be offered a target that sits on a window the user can't currently reach.
If we fix it
Tests correctly scope to whichever window (
wnd[N]) is actually active, and stop reading content sitting behind an open popup.Status
Already fixed and tested on PR #467 (
active_window/window-scoping logic +GuiMenufiltering, 4 new adapter tests, an 81-step example flow). This issue exists to track the bug independently of that PR, in case it stalls or gets reworked.Before closing
PR #467 already includes SAP adapter test coverage and a real example flow under
examples/sap/proving the fix — please keep that evidence attached to whichever PR closes this out.