diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 1515fe122..f28948868 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -277,7 +277,7 @@ namespace arith {
                 if (is_app(n)) {
                     internalize_args(to_app(n));
                     for (expr* arg : *to_app(n)) 
-                        if (a.is_arith_expr(arg))
+                        if (a.is_arith_expr(arg) && !m.is_bool(arg))
                             internalize_term(arg);
                 }
                 theory_var v = mk_evar(n);
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index f60c3597d..f6240993c 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -158,8 +158,9 @@ namespace euf {
         m_bool_var2expr[v] = e;
         m_var_trail.push_back(v);
         enode* n = m_egraph.find(e);
-        if (!n) 
-            n = m_egraph.mk(e, m_generation, 0, nullptr); 
+        if (!n) {
+            n = m_egraph.mk(e, m_generation, 0, nullptr);
+        }
         SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v);
         m_egraph.set_bool_var(n, v);
         if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
@@ -419,4 +420,13 @@ namespace euf {
         return g;
     }
 
+    euf::enode* solver::e_internalize(expr* e) {
+        euf::enode* n = m_egraph.find(e);
+        if (!n) {
+            internalize(e, m_is_redundant);
+            n = m_egraph.find(e);
+        }
+        return n;
+    }
+
 }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 080cd4a88..54a47476b 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -584,14 +584,16 @@ namespace euf {
         TRACE("euf", for (auto const& kv : replay.m) tout << kv.m_value << "\n";);
         for (auto const& [e, generation, v] : m_reinit) {
             scoped_generation _sg(*this, generation);
-            TRACE("euf", tout << "replay: " << v << " " << mk_bounded_pp(e, m) << "\n";);
+            TRACE("euf", tout << "replay: " << v << " " << e->get_id() << " " << mk_bounded_pp(e, m) << " " << si.is_bool_op(e) << "\n";);
             sat::literal lit;
             if (si.is_bool_op(e)) 
                 lit = literal(replay.m[e], false);
             else 
                 lit = si.internalize(e, true);
-            VERIFY(lit.var() == v);
-            
+            VERIFY(lit.var() == v);          
+            if (is_app(e))
+                for (expr* arg : *to_app(e))
+                    e_internalize(arg);
             attach_lit(lit, e);            
         }
         
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index f34819da3..3bf4d701a 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -348,6 +348,7 @@ namespace euf {
         void attach_node(euf::enode* n);
         expr_ref mk_eq(expr* e1, expr* e2);
         expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); }
+        euf::enode* e_internalize(expr* e);
         euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, m_generation, n, args); }
         expr* bool_var2expr(sat::bool_var v) const { return m_bool_var2expr.get(v, nullptr); }
         expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index 1538f9a3b..06efccaf0 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -218,12 +218,7 @@ namespace euf {
     }
 
     euf::enode* th_euf_solver::e_internalize(expr* e) {
-        euf::enode* n = expr2enode(e);
-        if (!n) {
-            ctx.internalize(e, m_is_redundant);
-            n = expr2enode(e);
-        }
-        return n;
+        return ctx.e_internalize(e);
     }
 
     unsigned th_euf_solver::random() {