[nils-loose]

What changed and why

When a recursion runs deep, the target's frames plus SWAT's per-instruction frames can use up the JVM stack. The StackOverflowError can then be thrown anywhere, including inside SWAT. Before this PR, the second overflow usually hit the lazy <clinit> of ErrorHandler, which then failed. That had three effects:

• The class stayed broken for the rest of the run, so every later error became NoClassDefFoundError.
• isActive stayed set.
• The target's error was replaced, so the target's own catch did not run.

Which outcome a run got was nondeterministic: either a halt (UNKNOWN), or a truncated trace sent with no marker, which is a false-SAFE hazard (stackoverflow-hits-errorhandler-clinit).

Executor

• ErrorHandler and the new StackOverflowGuard are initialized in premain, not on first use.
• processInstruction catches a StackOverflowError raised inside SWAT using only field writes. It swallows the error, so the target continues as it would without SWAT. Symbolic tracking stops for the rest of the run. isActive is now reset in finally.
• ErrorHandler passes a stack overflow on (it no longer halts or logs on an exhausted stack). This includes an ExceptionInInitializerError caused by an overflow.
• The exception handler of every instrumented call site records whether a StackOverflowError reached the target's code (DUP; INSTANCEOF; GETSTATIC; IOR; PUTSTATIC, with no call and no branch), before INVOKEMETHOD_EXCEPTION.
• A trace of such a run carries symbolicContextLoss, plus the new TraceDTO.stackOverflow flag when the error reached the target.

Explorer

• If the trace of a round has stackOverflow, the driver does not report that round's violation lines (an AssertionError under valid-assert, an uncaught RuntimeException under no-runtime-exception). It records them as the execution error stack_overflow_violation and keeps searching. Context loss still blocks SAFE.
• A run with no symbolic inputs that overflowed now ends UNKNOWN instead of SAFE.
• stats.json counts stack_overflow_traces.

Semantics. StackOverflowError is not a RuntimeException, so an uncaught one does not violate no-runtime-exception (G ! uncaught(java.lang.RuntimeException)). Whether a path overflows at all depends on the JVM's stack size, which the task does not fix:

• The plain JVM's maximum depth with the default 1 MB varies between about 9k (interpreted) and 18k (JIT).
• The labels assume an unbounded stack, except jayhorn-recursive/SatPrimes01 valid-assert, whose SAFE label holds only because the stack is bounded.

So an execution in which the target saw an overflow yields neither SAFE nor VIOLATION. A path where only SWAT overflowed and the target finished normally is a real execution: its violations stay valid, and only SAFE is blocked.

-Xss is unchanged. Instrumented reach is about 4.9k frames at 1 MB, 9.4k at 2 MB and 18.9k at 4 MB. A larger stack would not make any verdict sound: every overflow is already context loss. It would also make the deep rounds slower, because trace encoding is quadratic in depth (about 47 s for a 13.6k-branch trace at 1 MB). Finally, it could expose violations like SatPrimes01's that the labels exclude.

Measured

Setup: --sv-comp, 300 s, --mem15g, no SA, against baseline-results.jsonl. Runs measured: 1116.

• Affected set: all 76 runs of the KB tasks with the causes executor-stackoverflow, stackoverflow-hits-errorhandler-clinit, stackoverflow-not-modelled-as-program-outcome, executor-slow-or-nonterminating-run and uncaught-oom-huge-nondet-array, plus all of jayhorn-recursive.
• Regression set: all 1040 other runs that are correct in the baseline.

Result on this branch alone: 0 points gained, 0 lost, no new wrong verdicts. All 1040 baseline-correct runs are still correct.

task	prop	expected	base	new	points
jayhorn-recursive/Addition	NRE	SAFE	unknown	stall	0 → 0
jayhorn-recursive/SatAddition01	NRE	SAFE	unknown	stall	0 → 0
jayhorn-recursive/UnsatAckermann01	NRE	SAFE	unknown	stall	0 → 0
jayhorn-recursive/UnsatFibonacci01	NRE	SAFE	unknown	stall	0 → 0
jayhorn-recursive/SatFibonacci01	NRE / VA	SAFE	oom / ok	ok / oom	0 → 0 (memory classification noise)

Why the four runs flip from unknown to stall: the executor no longer halts, so the trace of the overflowing round is sent. On these runs it is longer than 3333 branches, which crashes the recursive tree construction (recursion-error-tree, fixed by fix/explorer-robustness). Combined with fix/explorer-robustness. I ran the 76 affected runs on two setups: this branch merged with fix/explorer-robustness, and fix/explorer-robustness alone on the base executor. Combined: +3 points against the baseline. Robustness fix alone: +2. No new wrong verdicts in either.

task	prop	expected	baseline	robustness only	combined
jayhorn-recursive/UnsatAckermann01	VA	VIOLATION	stall (0)	unknown (0): [SWAT Exception] after the overflow	violation (+1)
jayhorn-recursive/UnsatFibonacci01	VA	VIOLATION	stall (0)	violation (+1)	violation (+1)
jayhorn-recursive/UnsatFibonacci02	VA	VIOLATION	stall (0)	violation (+1)	violation (+1)

The other differences are 0-point:

• SatPrimes01 NRE: unknown with the robustness fix alone, timeout combined. The overflowing round no longer ends the run, so the search goes on.
• InfiniteLoop and SatFibonacci01: oom/ok memory-classification noise.

On its own the gain is soundness, not points. The overflow no longer replaces the target's error, the target's handlers run, and a truncated trace can no longer be taken for a complete path.

Tests

• StackOverflowAgentSpec (agentTest, forked agent with -Xss256k) covers a shallow recursion, an overflow caught by the target, and an uncaught overflow. On the base jar, the caught case prints no result, ends in NoClassDefFoundError(ErrorHandler), and the trace has no context loss.
• tests/test_stack_overflow.py covers driver violation suppression, other rounds, a SWAT exception, and no symbolic vars.
• ../gradlew test and agentTest pass. The explorer unit tests pass.

Known limits

• An overflow raised in the dispatcher frames that sit above processInstruction reaches the target as a StackOverflowError at a non-invoke instruction. It is still recorded by the next call-site handler.
• If the handler's own frames overflow, the exception in flight is replaced by a StackOverflowError. This also happens without this PR.
• The guard is global: an overflow in one thread stops tracking in all threads. SV-COMP targets are single-threaded.
• OutOfMemoryError (uncaught-oom-huge-nondet-array) is the target's own error, not this mechanism, and is unchanged.
• This PR conflicts with fix/explorer-robustness in Database.add_trace, ConstraintService.add_constraints and the no-symbolic-vars check of SVCompDriver. The conflicts are mechanical: keep both sides and pass stack_overflow through.

🤖 Generated with Claude Code

[nils-loose]

Included in dev through #92 (merge commit 534c182), together with the fixes for interactions between PRs. This PR stays as the record of the change and its measured flips.