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();
 }