[nils-loose]

What changes

DTOBuilder used to flag precision loss when any symbol in a branch constraint failed the name regex [A-Z].*_[0-9].*. It now decides from the kind each symbol was declared with.

• SymbolRegistry. Each symbol is declared, where it is created, as one of: INPUT, VALUE (another symbolic value), ARRAY_BASE, MODEL_FUNCTION (the definition holds for every argument) or APPROXIMATE_MODEL_FUNCTION. A branch constraint is imprecise if it mentions an approximate function or a symbol nobody declared. An undeclared symbol is logged once.

• Declarations:

  • Value.initSymbolic* declares VALUE.
  • SymbolicTraceHandler.addInput declares INPUT.
  • The array constructors declare ARRAY_BASE.
  • The String UFs (trimStart, trimEnd, commonPrefixLength, lastIndexOf) are MODEL_FUNCTION.
  • sin, cos, toLowerCase and equalsIgnoreCase are APPROXIMATE_MODEL_FUNCTION.

• Approximate models record precision loss where they add constraints. This now happens explicitly (recordSymbolicPrecisionLoss()), not only when a branch mentions the function:

  • SinCosUF restricts its argument to the sample points.
  • The guarded toLowerCase restricts chars to printable ASCII.
  • lastIndexOf(int) with a symbolic char is approximate (non-BMP and negative chars are not modelled).

  These constraints are trace-global, so they reach every query.

• Array base symbols get their own namespace ([I_alloc<n>, A_alloc<n>). An input array [I_<idx> can no longer share, and so constrain, an allocated array's base symbol.

Why this is sound: a precise symbol may still be under-constrained, for example a fresh value, an array base outside the stored range, or a partially defined function. That only over-approximates: UNSAT stays a proof. A model that does not reach its branch is a divergence, and an unexpected divergence already downgrades SAFE. Anything that may exclude real behaviour stays a precision loss.

Measured

• Setup: --sv-comp, --mem15g, 300 s, no SA. 1189 runs, compared with baseline-results.jsonl.
• Affected set (188 runs):
  • every non-correct KB run with precision-loss-false-positive-var-name, precision-loss-uf or array-base-symbol-collides-with-input;
  • every expected-VIOLATION run with precision loss in the baseline;
  • every expected-SAFE run that is not SAFE and has precision loss.
• Regression set: all 1001 baseline-correct runs (the change touches every run's DTO).

Result: +8 / -0, net +8, no new wrong verdicts. The one wrong verdict, AlbersProjection_true (SAFE -> VIOLATION), is the same as in the baseline.

task	prop	base	new	pts
jbmc-regression/StringCompare04	NRE	unknown	safe	+2
jbmc-regression/StringIndexMethods03	NRE	unknown	safe	+2
jbmc-regression/StringIndexMethods05	NRE	unknown	safe	+2
jdart-regression/array-iteration01	NRE	unknown	safe	+2

Soundness check:

• All 11 expected-VIOLATION runs where precision loss blocks a false SAFE keep the flag and stay UNKNOWN: coral*/Optimization* (sin/cos, sampled Math) and the two lastIndexOf(int) autostubs, which are now flagged by the explicit record.
• The flag was dropped on 13 runs, all already correct (9 VIOLATION, 4 SAFE).
• No run gained a precision-loss flag, so no undeclared symbol turned up.

Tests

• New SymbolRegistrySpec covering:
  • input and array base are precise, and the base name is outside the input namespace;
  • trim UFs are precise;
  • sin is a precision loss and records it;
  • an undeclared UF is a precision loss;
  • a later declaration does not weaken an input or an approximate one.
• Full executor test suite: 8735 tests, 0 failures.

Limits

• Most remaining KB runs with these causes are still blocked by context loss (collections, toLowerCase, StringBuffer) or by timeouts.
• The registry is a static map. It is not reset between threads. Names are unique per run.

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