From 7f7f8ae59bff21eccf04b08f45ca5bb210c635e2 Mon Sep 17 00:00:00 2001 From: "z3prover-ci-bot[bot]" <305651407+z3prover-ci-bot[bot]@users.noreply.github.com> Date: Tue, 21 Jul 2026 18:55:46 -0700 Subject: [PATCH] [snapshot-regression-fix] fpa: fp.to_bv of large-exponent values should be unspecified, not unknown (#10174) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## 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] >
> Firewall blocked 1 domain > > 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. > >
> 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) 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 | 7 +++++++ src/ast/rewriter/fpa_rewriter.cpp | 8 ++++++++ 2 files changed, 15 insertions(+) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index e255f4b108..533383484b 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/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); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index c2c888885b..3be70d4057 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/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);