[nils-loose]

What changes and why

Exact Math models (MathInvocation, checked against the JDK in MathInvocationSpec):

• Math.round rounded ties to even (round(2.5) = 2), but the JDK rounds them toward positive infinity. It is now floor(x) plus one if x - floor(x) >= 0.5, which is exact.
• max/min of floats and doubles used SMT-LIB fp.max/fp.min. Those return the other argument when one argument is NaN, and either zero for +0.0/-0.0. Both now follow the JDK definition.
• New: signum, and floorDiv/floorMod for int/long with a concrete non-zero divisor. A symbolic divisor would need a branch for the ArithmeticException, so it stays unmodelled (context loss).

Transcendental functions are per-call UFs (SampledMath, now including sin/cos):

• Each call is an application of its own function math_<name>_<n>(x).
• A trace constraint defines that function as the existing sample table: exact at the samples, the concrete result everywhere else.
• Precision loss is now recorded only when a branch constraint contains such a function (the existing UF check in DTOBuilder). A Math result that never reaches a branch no longer rules out SAFE.
• Each call has its own function, so the definitions never constrain each other or the inputs.
• SinCosUF is removed. Its trace-global constraint "the argument is one of the samples" also applied to branches before the call, and gave a false SAFE. Reproducer: if (x > 0.7 && x < 0.8) assert false; Math.sin(x); gives SAFE on the integration branch and VIOLATION here.

Explorer:

• UF definitions are sliced per query. A query keeps only the definitions whose functions it contains, transitively, plus any constraint without functions. This is sound because each left-out definition can be satisfied by its own function value.
• A query over a math_ function can only give a guess, and its trace is already precision loss. In sv-comp mode it gets at most --approximate-rlimit (default 2.5e8, about 1-1.5 min). If it runs out, the explorer gives up on that branch (UNKNOWN) and does not escalate the limit.
• The guess flag (expected divergence) now follows the query instead of the trace. A divergence from an exact query in a trace that had a Math call stays an error, so it still blocks SAFE.
• Function interpretations in a Z3 model are no longer read as input values.

Range axioms were not added. The table definition fixes the value at every argument, so axioms add no information. A free UF limited only by range axioms would give the solver guesses that diverge almost every time.

Measured

Competition config (nosa, 300 s, sv-comp.cfg, 15 GB), compared with baseline-results.jsonl. 437 runs:

• 337 affected: KB context-loss-math / precision-loss-uf / uf-global-constraints-unsliced / fp-encoding-imprecise, all float/coral/Math families, and the 25 runs that the SampledMath change had slowed to timeouts.
• 30 baseline-correct runs whose tasks use Math or the String UFs.
• 70 other baseline-correct runs.

task	prop	expected	base	branch	points
float-nonlinear-calculation/coral17	valid-assert	VIOLATION	unknown	violation	+1
float-nonlinear-calculation/coral21	valid-assert	VIOLATION	violation	unknown	-1
float-nonlinear-calculation/coral71	valid-assert	VIOLATION	violation	unknown	-1

• Net -1 (+1 / -2). No new wrong verdict. All three flips reproduce on a re-run.
  • coral21: the query needs more than the cap. It still runs out at 3.5e8.
  • coral71: the sin/cos sample set changed, the search takes another path, and it ends in DONT-KNOW.
• CPU: 47070 s -> 39911 s over the 437 runs (-15%). Timeouts: 140 -> 93.
• The 25 slowed runs: 7500 s -> 4408 s. 21 of them now end with UNKNOWN in 97-271 s instead of timing out. EulerMethod no-runtime-exception now ends in OOM (0 points, as before).
• Regression set: 0 flips, CPU 740 s -> 661 s.

Tests

• MathInvocationSpec: round, max/min, signum, floorDiv/floorMod against the JDK on edge values. It fails on the old models.
• tests/test_math_models.py: slicing, approximate-query cap, model extraction.
• Executor gradlew test and all explorer unit tests pass.

Known limits

• addExact/multiplyExact/... and floorDiv with a symbolic divisor are still unmodelled (context loss). They need a branch for the exception from inside a model. No current SV-COMP task uses them.
• copySign and hypot are not modelled.
• --approximate-rlimit is a trade-off: a higher cap recovers violations behind hard queries (coral21) but brings back long runs.
• The cap applies only in sv-comp mode.

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