[nils-loose]

Cuts the per-round cost of the SV-COMP loop (one executor JVM per round, then branch selection in the explorer). The verdict logic is unchanged. JVM reuse (#56) is out of scope.

Changes

Executor

• C1 only (-XX:TieredStopAtLevel=1, set in SVCompDriver.build_command). A round runs the target once, mostly for less than a second, and C2 compiles do not pay off in that time. A MinePump round drops from 1.58 to 0.95 executor CPU-s. Long executions are no slower (Hanoi with n=13/14: 13.6 -> 12.1 and 44 -> 42 CPU-s).
• No solver-context close at the end of an SV-COMP execution. The JVM exits right after the execution. Z3SolverContext.close (delContext) took 61% of a long-trace run (Hanoi n=14: 44 -> 12.5 CPU-s together with the next change).
• FormulaDumper: one Z3 solver for all trace formulas. java-smt's dumpFormula creates and initialises a new solver for every formula. The dumper uses one solver with push/assert/print/pop, then runs java-smt's own sanitize, so the output is identical. It falls back to dumpFormula if the reflective lookup fails. I checked the trace JSON of about 50 tasks from all families against the base jar: identical. The only differences were stack-overflow depths, which also vary from run to run on the base.
• DTOBuilder:
  • variables are extracted once per branch, with a precompiled input-name pattern;
  • compact JSON (still indented in PRINT mode);
  • constraint/inst/concreteOnly are left out when at their defaults (the explorer's pydantic defaults are the same).
• Null log manager for java-smt. BasicLogManager registers a JMX bean, which loads about 300 classes per run, and its log is never read.

Explorer

• Branch selection walks the Database's tree under the lock instead of a deep copy. Before, every round deep-copied the tree three times: once in select_branch and twice in determine_next_step, which only needs the count of symbolic variables. The driver keeps a shallow copy of the target node, so check_divergence still sees the side that was open when the branch was solved.
• is_symbolic_branch is memoised per (gid, trace_id). A non-symbolic open branch used to be re-checked and logged in every round.
• The per-node [DFS] line is only written when an SA graph is in use.
• _extract_variables is iterative and visits each subterm once (cherry-pick of 58c15ae from fix/explorer-robustness, same patch).

Measurements

Config: --sv-comp, --mem15g, nosa, 2 cores per run. Base is svcomp27/integration.

Speed (base and branch run side by side):

• 40 baseline timeouts at 60 s CPU, rounds per CPU-s:
  • median 1.56x, geomean 1.46x, p75 2.01x, p90 2.15x, max 6.93x;
  • on the 23 tasks with more than 5 rounds: median 1.85x, range 1.0-2.19x;
  • by family: MinePump 2.08x, TCAS 1.88x, jdart 1.85x, float_unboundedloop 1.52x;
  • unchanged (1.0x) where a run is stuck in one long solver query or execution (float-nonlinear, securibench).
• 40 quick correct runs: CPU per round 2.00 -> 1.20 s (median), total CPU 186 -> 109 s.
• All 1047 baseline-correct runs: total CPU 7687 -> 5040 s.

Verdicts

• Regression set, all 1047 baseline-correct runs: 0 changed, 0 new wrong verdicts.
• Timeout set, 229 of the 276 baseline timeouts (all except 47 of the 67 float-nonlinear-calculation runs, which are solver-bound):
  • 3 flips, +5 points, 0 lost, 0 new wrong verdicts;
  • all 3 re-run once on both sides with the same result.

task	prop	base	branch
argv-tasks/ProjectionGridRoundTripper_exceptionless	no-runtime-exception	timeout	SAFE (276 s)
float_unboundedloop/Adjustable-Inner-Count-Halving	valid-assert	timeout	VIOLATION (216 s)
jdart-regression/addition01	no-runtime-exception	timeout	SAFE (166 s)

Other changes, all 0 points:

• 3 jayhorn McCarthy91 runs: timeout -> UNKNOWN. Round 103 is reached sooner, and its input (I_0=-2147483647) overflows the stack inside the executor. The base jar does the same with that input.
• 2 SatHanoi01 runs: timeout -> stall. Round 4 now gets its trace to the explorer without spending the rest of the budget in delContext. Tree.add then hits RecursionError and the Database lock leaks. fix/explorer-robustness fixes that.

Tests

• New explorer unit tests in tests/test_round_overhead.py:
  • selection order and filtering;
  • no tree copy;
  • the memoised symbolic check;
  • the target snapshot;
  • variable extraction on shared and deep terms.
• Existing explorer tests pass.
• Executor test and agentTest pass.

Known limits

• Conflicts are likely with fix/explorer-robustness (Database with lock rewrite, DFS, ConstraintManager) and with branches that touch DTOBuilder/check_divergence. Each overlap is a few lines.
• The JVM floor is about 0.93 CPU-s per round: class loading and agent setup.
  • AppCDS cannot be used here: dumping needs the diagnostic AllowArchivingWithJavaAgent, and the benchmark class directories block it.
  • SerialGC/ParallelGC, -XX:-UsePerfData and CICompilerCount gave less than 2%. -Xverify:none was not adopted, since it would hide bad instrumented bytecode.
• Not addressed:
  • shadow-array-eager-copy-init: a constant-array initialisation changes what out-of-bounds selects mean and removes a precision-loss signal, so it needs its own soundness argument;
  • trace-encoding-quadratic-simplify: simplify is about 16% of a long-trace encode now.

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