From 7a302239c22097994002b97a046c8ad2921bf8f5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 26 Apr 2025 11:40:48 -0700
Subject: [PATCH] fix #7630

---
 src/tactic/tactic.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 0e0d93e90..f31757127 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -99,7 +99,12 @@ class lazy_tactic : public tactic {
     params_ref p;
     std::function<tactic* (ast_manager& m, params_ref const& p)> m_mk_tactic;
     tactic* m_tactic = nullptr;
-    void ensure_tactic() { if (!m_tactic) m_tactic = m_mk_tactic(m, p); }
+    void ensure_tactic() {
+        if (!m_tactic) {
+            m_tactic = m_mk_tactic(m, p);
+            m_tactic->updt_params(p);
+        }
+    }
 public:
     lazy_tactic(ast_manager& m, params_ref const& p, std::function<tactic* (ast_manager&, params_ref const&)> mk_tactic) : m(m), p(p), m_mk_tactic(mk_tactic) {}
     ~lazy_tactic() override { dealloc(m_tactic); }