From 99f64b80fa444defb47107d77ed8b791110f80e5 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Thu, 23 Apr 2026 16:17:21 +0200
Subject: [PATCH] Prevent unsound solve-eqs elimination across
 recursive-function definitions (#9358)

* Initial plan

* Prevent unsound solve-eqs elimination across recursive-function definitions

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/9a2fc92f-15e8-4806-988b-28bce96e8007

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update solve_eqs.cpp

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifiers/solve_eqs.cpp | 10 +++++++++-
 src/test/fpa.cpp                  | 14 ++++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index 2826e8ddd..ccbfb550a 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -244,10 +244,17 @@ namespace euf {
         unsigned count = 0;
         vector<dependent_expr> old_fmls;
         dep_eq_vector eqs;
+        struct reset_unsafe {
+            solve_eqs& s;
+            reset_unsafe(solve_eqs& s): s(s) {}
+            ~reset_unsafe() { s.m_unsafe_vars.reset(); }
+        };
+        reset_unsafe ru(*this);
         do {
             old_fmls.reset();
             m_subst_ids.reset();
             eqs.reset();
+            filter_unsafe_vars();
             get_eqs(eqs);
             extract_dep_graph(eqs);
             extract_subst();
@@ -265,6 +272,7 @@ namespace euf {
             old_fmls.reset();
             m_subst_ids.reset();
             eqs.reset();
+            filter_unsafe_vars();
             solve_context_eqs context_solve(*this);
             context_solve.collect_nested_equalities(eqs);
             extract_dep_graph(eqs);
@@ -334,7 +342,7 @@ namespace euf {
         m_unsafe_vars.reset();
         recfun::util rec(m);
         for (func_decl* f : rec.get_rec_funs())
-            for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m), &m_todo, &m_visited))
+            for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m)))
                 m_unsafe_vars.mark(term);
     }
 
diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp
index 12b423066..217cb641b 100644
--- a/src/test/fpa.cpp
+++ b/src/test/fpa.cpp
@@ -60,6 +60,20 @@ static void test_fp_to_real_denormal() {
         true);
 }
 
+static void test_recfun_defined_function_soundness() {
+    run_fp_test(
+        "(set-option :model_validate true)\n"
+        "(declare-fun fixedAdd () Int)\n"
+        "(declare-fun variableAdd () Int)\n"
+        "(define-fun-rec $$add$$ ((a Int) (b Int)) Int\n"
+        "  (ite (= 0 b) 2 (- a (+ 0 (- fixedAdd b)))))\n"
+        "(assert (= fixedAdd (* 9 fixedAdd)))\n"
+        "(assert (= 1 ($$add$$ 1 3)))\n"
+        "(check-sat)\n",
+        false);
+}
+
 void tst_fpa() {
     test_fp_to_real_denormal();
+    test_recfun_defined_function_soundness();
 }