From 6eeb274cd22a4d53990732233e382ca282aaa857 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Tue, 9 Jun 2026 10:22:03 -0700
Subject: [PATCH] Fix FPA incremental soundness for fp.to_* terms (#9022)
 (#9787)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #9022.

## Problem

After a `(push)`, Z3 could incorrectly report `unsat` for satisfiable
FPA formulas in which an uninterpreted function returns a floating-point
value (e.g. `int_to_fp`). The example in #9022 has a single `push` and a
single `check-sat` (no `pop`), so the `m_rw.reset()` added in
`pop_scope_eh` by #8712 does not apply.

## Root cause

`theory_fpa` lazily converts FP constraints to bit-vectors and asserts
the equivalences/side conditions as **unit theory axioms**
(`assert_cnstr` → `mk_th_axiom`, which `assign`s the literal at the
current decision level).

For `fp.to_*` terms (`fp.to_real`, `fp.to_ubv`, …) the conversion
equality and side conditions are emitted **only** in
`internalize_term()`, which runs exactly once. The `else if` branch for
fpa-family conversion terms in `relevant_eh` previously did nothing.

These unit axioms are level-local: on DPLL backtracking the assignment
is undone, but `internalize_term()` is not re-run for the
already-internalized term (in particular when the term lives at the
user-`push` base level, where its clause is not a reinit clause). The
side conditions include the axioms linking FP uninterpreted functions to
their bit-vector counterparts (`int_to_fp(i) =
fp(extract(int_to_fp_bv(i)))`). Once lost, `int_to_fp_bv` becomes
unconstrained, enabling an unsound `unsat`. This is exactly the behavior
described in #8345/#9022 (and why the result flips with vs. without
`push`).

## Fix

`relevant_eh` re-fires on relevancy re-propagation after a backtrack.
Re-emit the conversion equality and side conditions for `fp.to_*` terms
there, mirroring `internalize_term`, so the FP↔BV linking axioms stay in
force across backtracking. On an `m_conversions` cache hit this just
re-asserts the (hash-consed) conversion equality and a `true` side
condition, so it adds no new terms and no clause bloat. The change only
adds sound constraints, so it can never turn a satisfiable formula
`unsat`.

## Validation

- #9022 reproducer: no longer reports `unsat` across many random seeds
and longer timeouts; a model (`sat`) is still found (the problem is
inherently hard quantified FP + nonlinear arithmetic, so timeouts are
expected).
- #8345 reproducer: first `check-sat` still `unsat` (the negated
quantifier axiom is valid).
- Additional incremental push/pop FP cases with
`fp.to_real`/`fp.add`/`fp.sub` and FP-returning UFs: correct, consistent
results.
- `test-z3 /a`: all 89 unit tests pass.
- Debug build (soundness assertions enabled): no assertion failures on
the above cases.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/smt/theory_fpa.cpp | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 107456455..492595f60 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -494,6 +494,31 @@ namespace smt {
         else if (is_app(n) && to_app(n)->get_family_id() == get_family_id()) {
             // These are the conversion functions fp.to_* */
             SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
+
+            // The conversion equality and side conditions for fp.to_* terms are
+            // emitted in internalize_term(), which runs exactly once. Those are
+            // asserted as theory axioms at the current decision level and are
+            // undone on DPLL backtracking, while internalize_term() is not run
+            // again for the already-internalized term (e.g. when the term lives
+            // at the user push base level and its clause is not reinitialized).
+            // The side conditions include the axioms linking FP uninterpreted
+            // functions to their bit-vector counterparts; losing them leaves the
+            // BV counterpart unconstrained and causes an incremental-mode
+            // soundness bug. relevant_eh re-fires on relevancy re-propagation
+            // after a backtrack, so re-emit them here to keep them in force.
+            switch ((fpa_op_kind)to_app(n)->get_decl_kind()) {
+            case OP_FPA_TO_FP:
+            case OP_FPA_TO_UBV:
+            case OP_FPA_TO_SBV:
+            case OP_FPA_TO_REAL:
+            case OP_FPA_TO_IEEE_BV: {
+                expr_ref conv = convert(n);
+                assert_cnstr(m.mk_eq(n, conv));
+                assert_cnstr(mk_side_conditions());
+                break;
+            }
+            default: /* ignore */;
+            }
         }
         else {
             /* Theory variables can be merged when (= bv-term (bvwrap fp-term)),