[nils-loose]

What changes

Explorer: retry diverged branches. When the run of a solution does not take the side of the branch it was solved for, the branch used to stay "solved", so its unexplored side was never tried again, and since #65 (18b0af7) SAFE is ruled out. Now the branch becomes a candidate again, up to --divergence-retries times (default 3):

• a retry excludes every solution that failed so far (a blocking clause over the scalar inputs of each failed model);
• it tries small values first: integral inputs bounded by 16, 256 and 65536 in turn, then unbounded;
• UNSAT under these extra constraints proves nothing, so it is never recorded as an infeasible branch.

Only when all retries diverge, or no other solution is left, is the branch given up on. That is recorded as unexpected_divergence, or as an expected divergence for an approximate model, as before. A given-up branch rules out SAFE, unless another run reached its unexplored side by the end of the search. In that case the side is in the tree, so the search covered it like any other.

Executor: FCMPG/FCMPL encode NaN and signed zeros. The formula had no NaN case, so a NaN operand compared as "less", while the JVM pushes 1 (FCMPG) or -1 (FCMPL). Z3 could then pick NaN to satisfy 0.0f <= x, and the run took the other side. The concrete value used Float.compareTo, which orders -0.0f below 0.0f. The fix mirrors DoubleValue.DCMP. A concrete NaN operand also no longer drops the formula.

Why the runs diverged

• 17 algorithms runs (InsertionSort, MergeSortIterative, BellmanFord-*02, Tsp): Z3 picks a size such as 2^31-1 or 524288, and the allocation throws OutOfMemoryError before the run reaches the branch. Retries with small sizes reach the branch. These tasks have an unbounded nondet size, though, so a sound SAFE is not reachable for the SAFE runs. They now end in timeout, or in a stall from the known RecursionError in Tree.add_recursive, instead of UNKNOWN. Both score 0. Four valid-assert VIOLATIONs are now found.
• Piecewise_true: the FCMP NaN encoding described above.

Soundness

• SAFE still requires every branch to be covered or proven UNSAT. A query with retry constraints never marks a branch infeasible.
• A given-up branch blocks SAFE unless its side was reached by some run.
• The existing downgrades are unchanged: context loss, precision loss (approximate traces), sa_desync and uncaught exceptions.

Measurements

Configuration: --sv-comp, 300 s CPU, mem15g, no SA. Compared against baseline-results.jsonl of the integration branch.

• Affected set, 209 runs: every run with a divergence in the Static pre-analysis pruning, with soundness fixes #65 re-run, plus the KB causes diverged-branch-not-retried, missing-violation-after-exhaustion, search-strategy-misses-violation, branch-divergence, solver-model-unbounded-values and fcmp-nan-unordered-not-encoded. Result: +19 / -0.
• Regression set, 200 runs: baseline runs with any divergence, baseline-correct float and argv runs, unsolved expected-false float and argv runs, and 70 random baseline-correct runs. Result: +1 / -4. The flips were re-run once on both sides and reproduced.
• Total: +20 / -4, net +16, no new wrong verdicts.

task	prop	base	new	pts
argv-tasks/Piecewise_true	both	unknown	safe	+4
argv-tasks/FractalTouchHandler_true	both	unknown	safe	+4
argv-tasks/ReverseInterpolator_false	NRE	timeout	safe	+2
argv-tasks/ReverseInterpolator_false2	NRE / valid	timeout	safe / violation	+3
algorithms/InsertionSort-{Fun,Mem}Unsat01	valid	unknown	violation	+2
algorithms/MergeSortIterative-{Fun,Mem}Unsat01	valid	unknown	violation	+2
float-nonlinear-calculation/coral17, coral43	valid	unknown	violation	+2
argv-tasks/DiskBasedCache	valid	timeout	violation	+1
argv-tasks/AbstractChart_exceptionless	NRE	safe	timeout	-2
argv-tasks/TouchPadView	valid	safe	timeout	-2

Credit for the gains:

• FCMP fix: Piecewise, FractalTouchHandler, ReverseInterpolator, DiskBasedCache.
• Retries: algorithms, coral17, coral43.

Tests

• tests/test_divergence.py (rewritten, 21 tests): the retry and give-up flow, guesses, a side reached later, bound order, LIMIT and UNKNOWN handling, retry_constraints on a real Z3 instance (exclusion, bounds, strings and doubles), and UNSAT under extra constraints not being recorded.
• tests/test_solver_rlimit.py and test_sa_walk.py pass.
• FloatValueTest gains symbolic NaN and signed-zero cases for FCMPG/FCMPL. They fail without the fix.

Known limits

• Losses from the FCMP fix: AbstractChart_exceptionless and TouchPadView lose a SAFE (-4). No retries happen there. The exact NaN case makes NaN paths reachable and makes the FP queries much harder (0.3 s becomes about 70 s per query).
• Retries cost rounds: runs that used to stop early at UNKNOWN now spend their time on small-size retries. That is score-neutral, but they end as timeout or stall.
• What the blocking clause covers: it is over scalar inputs only. Arrays are not used to tell models apart, which can only over-restrict a retry.

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