diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index b4f6a2309..bc8f9ea64 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3198,14 +3198,15 @@ namespace smt {
 
     void context::internalize_assertions() {
         if (get_cancel_flag()) return;
+        if (m_internalizing_assertions) return;
+        flet<bool> _internalizing(m_internalizing_assertions, true);
         TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
         timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
         reduce_assertions();
         if (get_cancel_flag()) return;
         if (!m_asserted_formulas.inconsistent()) {
-            unsigned sz    = m_asserted_formulas.get_num_formulas();
             unsigned qhead = m_asserted_formulas.get_qhead();
-            while (qhead < sz) {
+            while (qhead < m_asserted_formulas.get_num_formulas()) {
                 if (get_cancel_flag()) {
                     m_asserted_formulas.commit(qhead);
                     return;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 2fb888bc3..7ca2e1c63 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -107,11 +107,12 @@ namespace smt {
 
         ptr_vector<justification>   m_justifications;
 
-        unsigned                    m_final_check_idx; // circular counter used for implementing fairness
+        unsigned                    m_final_check_idx = 0; // circular counter used for implementing fairness
 
-        bool                        m_is_auxiliary { false }; // used to prevent unwanted information from being logged.
-        class parallel*             m_par { nullptr };
-        unsigned                    m_par_index { 0 };
+        bool                        m_is_auxiliary = false; // used to prevent unwanted information from being logged.
+        class parallel*             m_par = nullptr;
+        unsigned                    m_par_index = 0;
+        bool                        m_internalizing_assertions = false;
 
         // -----------------------------------
         //
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index d86594f0f..d87a4f971 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -615,11 +615,15 @@ namespace smt {
 
     bool context::has_lambda() {
         for (auto const & [n, q] : m_lambdas) {
-            if (n->get_class_size() != 1) 
+            if (n->get_class_size() != 1) {
+                TRACE("context", tout << "class size " << n->get_class_size() << " " << enode_pp(n, *this) << "\n");
                 return true;
+            }
             for (enode* p : enode::parents(n)) 
-                if (!is_beta_redex(p, n)) 
+                if (!is_beta_redex(p, n)) {
+                    TRACE("context", tout << "not a beta redex " << enode_pp(p, *this) << "\n");
                     return true;
+                }
         }
         return false;
     }
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index e71630fa4..a05fbc68d 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -498,6 +498,8 @@ namespace smt {
             return p->get_arg(0)->get_root() == n->get_root();
         if (is_map(p))
             return true;
+        if (is_store(p))
+            return true;
         return false;
     }