[solid-eureka]

Implements the plan from #93: the static property pre-check moves into cfg-extraction, the check and the static pre-analysis graph share instruction facts, and the graph can prune under no-runtime-exception. It also fixes two walk desyncs that came up on the way.

It needs the matching cfg-extraction branch issue-93-precheck-in-cfg-extraction.

Changes

Step 1: the pre-check lives in cfg-extraction

• The explorer runs cfg-extraction's cfg-extractor-precheck.jar (--precheck-jar, or found next to symbolic-explorer/, or in ../cfg-extraction/build/libs/). The executor no longer contains the check.
• The SV-COMP archive ships the jar. CI builds it at the cfg-extraction tag pinned in cfg-extraction.ref.

Step 2: shared facts between the check and the graph

• cfg-extraction marks graph nodes that cannot raise a RuntimeException (cannotRaise), from the check's value analysis.
• SAGraph turns the exception side of such guards into a dead end.

Step 3: pruning under no-runtime-exception

• The graph's target points are chosen by property: runtimeExceptionPointIds (the sites that may raise a RuntimeException, plus uncaught[T] of RuntimeException types) under no-runtime-exception.
• In the harness it is opt-in: svcomp test run --sa-no-runtime-exception.

Walk desyncs

• Branches inside SWAT's helpers (UtilInstrumented.refEquals) are flagged like callbacks, since their number depends on runtime types. cfg-extraction drops its outdated two-branch model of the helper.
• cfg-extraction expands Verifier.nondetObject into the factory it calls, as the executor runs it.

Results

SA on, 300 s per task, before and after the changes in this branch:

Suite	Before	After
valid-assert (978): tasks with an SA desync	73	0
valid-assert: correct verdicts	812	814
sa-soundness (120): correct verdicts	114	115
no-runtime-exception (736) with SA: correct verdicts	(not run before)	654, the same as without SA

• No false SAFE in any run. The remaining false alarms are the mislabelled tasks in Expected verdicts of PieSegment_true and AlbersProjection_true #63.
• The pre-check gives identical results before and after the move on all 1342 tasks. Its release gate (cfg-extraction scripts/precheck_gate.py) finds 426 + 3 proofs with 0 contradictions.
• Under no-runtime-exception, SA cuts the queries on solved SAFE tasks by a third but solves nothing new at 300 s (the pre-check already proves 426 tasks, and the extractor costs 3 to 6 s per task). That is why it is opt-in.
• Tests: executor 11025 unit tests and 36 agent specs, explorer tests and cfg-extraction tests pass.

Before merging

1. CI access to cfg-extraction. The build job needs a secret CFG_EXTRACTION_TOKEN with read access to the private cfg-extraction repository, or the repository has to become public. Until then CI fails at "Check out cfg-extraction" and skips the test and package jobs.
2. The tag. cfg-extraction.ref names v0.1.0, which does not exist yet.
3. A license for cfg-extraction, since its code now ships in the public archive.

Note

This branch is based on niklas/dev, so the PR also contains its six commits that are not in dev yet (string encodings and Int2BvLifting, Z3 5.3.1 in the harness, --search-order, --prefer-short-strings). e9dec3d (char codes lifted without modulo) may overlap with #99.

🤖 Generated with Claude Code