From b16e142127bffd87391a35909307643a9c13b75e Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 21 Feb 2026 02:45:20 +0000
Subject: [PATCH 1/2] Initial plan


From 46daa160edb98da81bdf55c6506ddcbd50266fcd Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 21 Feb 2026 03:35:47 +0000
Subject: [PATCH 2/2] Fix FPA soundness issue: reset rewriter cache in
 pop_scope_eh (issue #8345)

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

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 5afc26c97..ec64bfd61 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -414,6 +414,12 @@ namespace smt {
     void theory_fpa::pop_scope_eh(unsigned num_scopes) {
         m_trail_stack.pop_scope(num_scopes);
         TRACE(t_fpa, tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";);
+        // Reset the fpa2bv rewriter cache so that expressions re-converted after
+        // a pop regenerate their side conditions (extra_assertions). Without this,
+        // the rewriter returns cached results without invoking mk_uf/mk_const and
+        // the axioms connecting FP UFs to their BV counterparts are never re-emitted,
+        // causing a soundness issue in incremental mode.
+        m_rw.reset();
         theory::pop_scope_eh(num_scopes);
     }