[snapshot-regression-fix] fpa: fp.to_bv of large-exponent values should be unspecified, not unknown (#10174)

## Summary

Fixes a completeness regression where a **satisfiable** floating-point
problem is answered `unknown`.

- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3232
- **Benchmark:** `iss-3199/bug-1.smt2` (from
https://github.com/Z3Prover/z3/issues/3199)

### Divergence

```diff
--- bug-1.expected.out (expected)
+++ produced (current z3)
@@ -1 +1 @@
-sat
+unknown
```

The benchmark:

```smt2
(declare-fun x () (_ FloatingPoint 40 60))
(declare-fun y () (_ BitVec 8))
(assert (= ((_ fp.to_ubv 8) RTP x) y #x00))
(check-sat)
```

`(get-info :reason-unknown)` reports `"exponents over 31 bits are not
supported"`.

### Root cause

The problem is clearly `sat` (e.g. `x = 0.0`, `y = #x00`; and for any
out-of-range `x`, `fp.to_ubv` is unspecified so `= #x00` is
satisfiable). z3 bit-blasts and finds a model that assigns `x` a value
with a very large binary exponent (the `FloatingPoint 40 60` sort has a
40-bit exponent field). During model reconstruction,
`fpa_util::is_considered_uninterpreted` performs a range check by
calling `mpf_manager::to_sbv_mpq`, which **throws** `"exponents over 31
bits are not supported"` when the unpacked exponent does not fit into an
`int` (guard added in `eacde16b` for #3199). The tactic framework
catches that exception and turns the whole result into `unknown`,
instead of treating the conversion as out-of-range/unspecified.

### Fix

A finite FP value whose (unbiased) binary exponent is at least the
target bitwidth `bv_sz` has magnitude `>= 2^bv_sz` and therefore cannot
fit into a `bv_sz`-bit signed or unsigned integer — the conversion is
unspecified. Short-circuit this case using the exponent, before reaching
`to_sbv_mpq`, in the two range-check paths:

- `src/ast/fpa_decl_plugin.cpp`
(`fpa_util::is_considered_uninterpreted`) — return `true` (considered
uninterpreted / out of range).
- `src/ast/rewriter/fpa_rewriter.cpp` (`fpa_rewriter::mk_to_bv`) —
return the unspecified result.

This is consistent with the existing precise logic for every exponent it
covers (those values are already classified out-of-range), and it avoids
materializing an astronomically large integer. It does not affect
in-range or boundary conversions.

### Validation

Built z3 from this checkout (Python/`make` build) and re-ran the
benchmark:

- `z3 -T:20 inputs/issues/iss-3199/bug-1.smt2` now prints `sat`,
matching the recorded `bug-1.expected.out` oracle.

Additional manual sanity checks (all correct, no regression):

- `fp.to_ubv 8` of `5.0` -> `#x05`
- `fp.to_sbv 8` of `-5.0` -> `#xfb` (-5)
- `fp.to_sbv 8` of `128.0` -> unspecified (`sat`, out of range)
- `fp.to_sbv 8` of `-128.0` -> `#x80` (-128, in-range boundary
preserved)

Opened as a **draft** for human review.




> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
>   allowed:
>     - defaults
>     - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>


> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/29804584327)
· 314.9 AIC · ⌖ 20.3 AIC · ⊞ 10.7K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)

<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
29804584327, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/29804584327 -->

<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->

Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/ast/fpa_decl_plugin.cpp

@@ -1091,6 +1091,13 @@ bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* cons
         scoped_mpf sv(fm());
         if (!is_rm_numeral(rm, rmv) || !is_numeral(x, sv)) return false;
         if (is_nan(x) || is_inf(x)) return true;
+        // A finite value whose (unbiased) binary exponent is at least bv_sz has
+        // magnitude >= 2^bv_sz, so it cannot fit into a bv_sz-bit signed or
+        // unsigned integer and the conversion is unspecified. Detect this here to
+        // avoid calling to_sbv_mpq, which rejects exponents that do not fit into
+        // an int (throwing "exponents over 31 bits are not supported").
+        if (plugin().fm().exp(sv) >= (mpf_exp_t)bv_sz)
+            return true;
         unsynch_mpq_manager& mpqm = plugin().fm().mpq_manager();
         scoped_mpq r(mpqm);
         plugin().fm().to_sbv_mpq(rmv, sv, r);

src/ast/rewriter/fpa_rewriter.cpp

@@ -721,6 +721,14 @@ br_status fpa_rewriter::mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool i
         if (m_fm.is_nan(v) || m_fm.is_inf(v))
             return mk_to_bv_unspecified(f, result);
 
+        // A finite value whose (unbiased) binary exponent is at least bv_sz has
+        // magnitude >= 2^bv_sz and therefore does not fit into a bv_sz-bit signed
+        // or unsigned integer; the conversion is unspecified. Handle it here to
+        // avoid calling to_sbv_mpq, which rejects exponents that do not fit into
+        // an int (throwing "exponents over 31 bits are not supported").
+        if (m_fm.exp(v) >= (mpf_exp_t)bv_sz)
+            return mk_to_bv_unspecified(f, result);
+
         bv_util bu(m());
         scoped_mpq q(m_fm.mpq_manager());
         m_fm.to_sbv_mpq(rmv, v, q);