Fix FPA soundness issue in incremental solving with push/pop

[Copilot]

After a (push), Z3 incorrectly reports unsat for satisfiable FPA formulas involving uninterpreted functions returning floating-point values. The root cause is that side conditions generated by mk_uf (which connect FP UFs to their BV counterparts) are asserted as scoped CLS_TH_AXIOM clauses that get deleted on DPLL backtrack, but the m_conversions cache retains entries at the base scope level and short-circuits the rewriter — preventing side conditions from being re-emitted.

Root Cause

The PR #8712 fix (m_rw.reset() in pop_scope_eh) only helps when m_conversions does not have a cached entry. theory_fpa::convert() checks m_conversions before calling the rewriter, so if an entry exists at base scope (scope 1, after user push), the rewriter is never invoked, mk_uf is never called, and no side conditions are added to m_extra_assertions. Meanwhile, the side conditions originally asserted during that conversion (at a deeper DPLL scope) have been deleted by backtracking.

Additionally, context::internalize_term is a no-op for already-internalized terms (returns early if e_internalized(n)), so side conditions from the first internalization of terms like (fp.to_real (fp.add ...)) are never re-asserted after backtracking removes the associated clauses.

Change

In theory_fpa::pop_scope_eh, clear m_conversions in addition to resetting m_rw, so all conversions are re-run after any pop and side conditions are unconditionally re-emitted:

void theory_fpa::pop_scope_eh(unsigned num_scopes) { m_trail_stack.pop_scope(num_scopes); m_rw.reset(); // Clear m_conversions so side conditions are regenerated after pop; // m_converter.m_uf2bvuf is preserved for consistent BV UF reuse. dec_ref_map_key_values(m, m_conversions); theory::pop_scope_eh(num_scopes); }

The converter's m_uf2bvuf map (FP UF → BV UF mapping) is intentionally preserved to ensure the same BV function is reused across re-conversions, maintaining consistency.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>FPA soundness issue in incremental solving still exists</issue_title>
<issue_description>Unfortunately, PR #8712 did not solve issue #8345 (I cannot reopen the issue) for the examples posted in the issue.

For example, the solver still incorrectly reports unsat in the following example. Removing the push changes the output to sat:

(declare-fun int_to_fp (Int) (_ FloatingPoint 5 11)) ; Definition of int_to_fp as composition of int2bv and to_fp (assert (forall ((i Int)) (! (= (int_to_fp i) ((_ to_fp 5 11) ((_ int2bv 16) i))) :pattern ((int_to_fp i)) :qid |int_to_fp_def| ))) ; Should trivially follow from the axiom above, but for some reason required for the issue (assert (forall ((i Int) (j Int)) (! (and (= (fp.to_real (fp.add RNE (int_to_fp i) (int_to_fp j))) (fp.to_real (fp.add RNE ((_ to_fp 5 11) ((_ int2bv 16) i)) ((_ to_fp 5 11) ((_ int2bv 16) j))))) (= (fp.to_real (fp.sub RNE (int_to_fp i) (int_to_fp j))) (fp.to_real (fp.sub RNE ((_ to_fp 5 11) ((_ int2bv 16) i)) ((_ to_fp 5 11) ((_ int2bv 16) j))))) ) :pattern ((int_to_fp i) (int_to_fp j)) :qid |int_to_fp_ax| ) )) (push) (declare-fun triggering_term ((_ FloatingPoint 5 11)) (Bool)) (assert (triggering_term (int_to_fp 16384))) ; 2.0 (assert (triggering_term (int_to_fp 15820))) ; ~0.1 (check-sat) ```</issue_description> <agent_instructions>If you have a fix, create a pull request.</agent_instructions> ## Comments on the Issue (you are @copilot in this section) <comments> </comments> 

• Fixes FPA soundness issue in incremental solving still exists #9022

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.