[nils-loose]

Fixes #87

What changed

When the target JVM failed before main ran (VerifyError, ClassNotFoundException: Main, a task that did not compile in the competition package, an agent crash in premain), no trace reached the explorer. The SV-COMP driver then saw zero symbolic variables, took the run for a non-symbolic program (== NON-SYMBOLIC), and reported SAFE.

The executor sends a trace whenever the entry method was entered, also when the method ends in an exception (surrounding try/catch, then Intrinsics.terminate) or in System.exit (shutdown hook). The trace POST is synchronous. So a trace arriving during a round is the positive signal that main ran.

• Database.trace_count() is new. run_testcase compares the count before and after each target run.
• A round with no new trace records a no_trace execution error in stats.json and ends with UNKNOWN. This check runs after the output scan, so an AssertionError that the program itself throws before main (for example in the main class's static initializer) is still reported as VIOLATION. A [SWAT Exception] or SWAT assertion still gives UNKNOWN, as before.
• The divergence check is skipped for such a round, because the latest trace in the database belongs to an earlier round.
• run_swat.py only relays the explorer's verdict line, so the competition package is covered by the same change.

Measurement

360 runs, competition config (--sv-comp, 300 s, mem15g, nosa), compared with the baseline:

• all 194 baseline runs that went through the NON-SYMBOLIC path (all correct SAFE; every one received a trace);
• all 86 baseline runs that received no trace (all already UNKNOWN or stall, through [SWAT Exception] and similar);
• 80 random baseline-correct runs (40 SAFE, 40 VIOLATION).

No run in the set hit the new no_trace path, so no verdict changes on the benchmarks. Three cases came out different, and none of them is a real verdict change:

task	prop	base	new	after re-run
argv-tasks/Constant_true	valid-assert	safe	unknown	safe on both sides (the batch had been interrupted, so this log dir held two runs)
securibench/Inter14	no-runtime-exception	stall	unknown	0 points either way
securibench/Inter14	valid-assert	stall	unknown	0 points either way

Net: 0 points, 0 new wrong verdicts.

Reproducers, base vs. this branch:

target	base	new
VerifyError (Main compiled against B extends A, run with a B that does not extend A)	SAFE	UNKNOWN
No class Main (explorer)	SAFE	UNKNOWN
No class Main / task does not compile (run_swat.py, ClassNotFoundException: Main)	SAFE	UNKNOWN
Non-symbolic program that runs to completion	SAFE	SAFE

Tests

• symbolic-explorer/tests/test_no_trace.py: unit tests for determine_next_step and for how run_testcase derives received_trace.
• symbolic-explorer/tests/test_failed_start_e2e.py: the reproducers above, run end to end through the explorer and through the package wrapper (run_swat.py in the package layout). Skipped when the executor jar, the Z3 libraries or javac are missing. The failed-start cases fail on the base and pass here.
• The existing explorer tests (divergence, solver rlimit, SA walk) pass.

Known limits

• With the abort timer enabled (useAbortTimer, off in sv-comp.cfg), an aborted run sends no trace and now gives UNKNOWN instead of SAFE.
• A target that crashes in a way that also breaks sending the trace (for example a native crash) now gives UNKNOWN. This is sound, and no such run appeared in the measured set.

🤖 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.