[nils-loose]

Z3's default solver bit-blasts floating point eagerly only for pure QF_FP/QF_FPBV queries. An uninterpreted function (the SampledMath models) or a string term (parseFloat) in an FP query makes it fall back to the lazy theory_fpa of the SMT core, which is much slower on these queries.

Changes

• Z3Handler.solve gives every query that contains an FP- or RoundingMode-sorted term to Tactic('qffp').solver() first, through the new Z3Handler.check_query. Whatever remains after bit-blasting (strings, Int arithmetic, arrays, UFs) is handled by the SMT core at the end of the tactic pipeline.
• Whether a query has FP terms is computed once per cached constraint and kept in its cache entry (iterative walk over the C API, no global AST-id memo).
• SAT is accepted only if the model satisfies every assertion, both before and after the int2bv lifting (model_completion=True, evaluated on a copy so the reported inputs are unchanged). Otherwise the default solver decides.
• UNSAT is trusted as from the default solver: the qffp pipeline (simplify, propagate-values, fpa2bv, bit-blast, SAT/SMT) is a satisfiability-preserving transformation by Z3's own fpa2bv, the same one the default solver applies to pure QF_FP. There is no cheap independent check; no SAT/UNSAT disagreement was found on the corpus below.
• An unknown caused by rlimit, timeout or a ResourceBudget interrupt is returned as before (LIMIT/UNKNOWN distinction unchanged), with no second attempt. Any other unknown, or a Z3 exception, falls back to the default solver with the remaining timeout and rlimit.
• rlimit units: the tactic decides FP queries with far fewer units, so a fixed rlimit (e.g. --approximate-rlimit) reaches further.
• --no-fp-tactic switches it off (on by default).

Measured

• 748 queries from SV-COMP runs (248 with FP terms), 10 s cap: FP queries decided 207 instead of 161, in 680 s instead of 1104 s CPU. No SAT/UNSAT disagreement with the default solver, no rejected model, no fallback triggered.
• End to end (valid-assert, 300 s): coral16, coral22 and Optimization3 go from UNKNOWN/timeout to a correct VIOLATION; with --no-fp-tactic coral16 is UNKNOWN again.
• Tests: 27 new unit tests in tests/test_fp_tactic.py (selection incl. FP+UF/strings/arrays, model shape, fallback on unknown/exception/wrong model, no fallback on limit/timeout/interrupt, a real FP+UF core). Explorer suite: 227 passed, 6 skipped (dev: 200 passed, 6 skipped).

Full-campaign numbers follow in a comment.

🤖 Generated with Claude Code

[nils-loose]

Full campaign: 1713 SV-COMP jobs (300 s CPU, no SA, sv-comp.cfg, 15 GB / -Xmx12g), dev 209cc0e and svcomp27/overnight-solver-perf (dev + #96 + #98 + #99) run at the same time, 16 slots x 2 cores each.

	dev	dev + #96 + #98 + #99
points	2192	2201 (+9)
correct SAFE / VIOLATION	804 / 664	804 / 673
wrong (5 known wrong labels, #63)	5	5
new wrong verdicts		0
timeouts / UNKNOWN	136 / 103	127 / 103
CPU sum	46431 s	40090 s (-14%)

Attribution: the 20 runs that changed were re-run with each change switched off (--no-fp-tactic, --no-executor-cds, without #99).

This PR accounts for all verdict changes (with --no-fp-tactic all of them revert to dev; reproducible on a second run):

• +10: EquidistantConicProjection_false, Optimization3, coral16/22/33/56/57/61/62, juliet CWE369 float_console_readLine_divide_54_bad_version2 (valid-assert): UNKNOWN/timeout -> correct VIOLATION.
• -1: coral21 valid-assert VIOLATION -> UNKNOWN. The path goes through approximate (SampledMath) Math models; with qffp the solver returns different models, all 4 diverge and the explorer gives up (precision loss). Not a soundness issue; the same mechanism keeps coral49/50/51/81 and Optimization2 at UNKNOWN/timeout.
• 0: 9 juliet CWE369 float SAFE runs go from timeout to UNKNOWN in 35-93 s (parseFloat precision loss prevents SAFE).
• No fallback (bad model, exception, unknown) logged in any run.

float-nonlinear-calculation CPU -47%, juliet-java -50%.

🤖 Generated with Claude Code