[nils-loose]

The SV-COMP 2027 version, in one block. It is a fast-forward of dev; the previous dev state is tagged pre-svcomp27.

Contents

• Write witnesses from the trace via witnesscreator #58: witnesses written from the trace via witnesscreator. This includes Make SV-COMP archive run on Ubuntu 26.04 #52, the Ubuntu 26.04 archive.
• Static pre-analysis pruning, with soundness fixes #65: static pre-analysis pruning.
• Support Verifier.nondetObject in the SV-COMP instrumentation #66–Model StringBuffer, ignore-case comparisons, simple regexes and more String methods #90: soundness, precision and performance fixes, one draft PR each. Their bases are svcomp27/integration (= dev + Write witnesses from the trace via witnesscreator #58 + Static pre-analysis pruning, with soundness fixes #65), feat/bitop-models and fix/string-model-soundness.
• Interaction fixes that exist only here, for problems that appear only when two PRs are combined:
  • Make the explorer robust: iterative tree, lock safety, crashes end UNKNOWN #72 + Loop-head state matching for concrete loop states #84: the loop-state matching in the iterative walk;
  • Static property pre-check: SAFE for programs proven free of RuntimeExceptions or AssertionErrors #73 + Report UNKNOWN when the target never reaches main #89: a failed start stays UNKNOWN;
  • Retry diverged branches; encode NaN in FCMPG/FCMPL #74 + Cut per-round overhead of the executor and explorer #82: the snapshot keeps the node reference;
  • Decide precision loss by symbol kind instead of by variable name #71 + Exact Math models, per-call UFs for transcendental functions, bounded queries over them #80: the math UFs are approximate;
  • Make the explorer robust: iterative tree, lock safety, crashes end UNKNOWN #72 + Handle StackOverflowError in the target as the plain JVM would #78: the stack overflow is kept on a failed ingest;
  • Model parsing numbers from Strings, with NumberFormatException as a branch #83 + Model StringBuffer, ignore-case comparisons, simple regexes and more String methods #90: the parse branches.
• Dependency update:
  • Z3 4.15.4 → 5.3.1 in the executor and the explorer. The explorer keeps the previous regex solver (smt.seq.regex_monadic=false).
  • JavaSMT 6.0.0 plus upstream fix 3113516df, vendored in libs/maven.
  • ASM 9.11.1, Jackson 2.22.4, logback 1.6.5, SLF4J 2.0.20, Spock 2.5, Mockito 5.24.
  • Gradle 8.14.6 and the build plugins.
  • The Python dependencies and the CI actions.

Measured

Full set of 1713 runs: --sv-comp, 300 s CPU, 15 GB, no SA.

	dev + #58 + #65	This branch
Points	1497	2192
Correct verdicts	1047	1468
Timeouts / stalls / OOM	276 / 37 / 11	137 / 0 / 0

• The 5 wrong verdicts are all wrong task labels (Expected verdicts of PieSegment_true and AlbersProjection_true #63).
• Compared with the same fixes on the old dependency versions: +8 points, 0 new wrong verdicts.

Tests

• Executor 11013 passed, agentTest 34/34, explorer 206 OK.
• The package passes check-svcomp-package.sh in docker.io/ubuntu:26.04.

🤖 Generated with Claude Code