diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 5a8a313ba..ffaee434f 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -198,11 +198,19 @@ namespace smt {
         if (get_depth(n) > DEEP_EXPR_THRESHOLD) {
             // if the expression is deep, then execute topological sort to avoid
             // stack overflow.
+            // a caveat is that theory internalizers do rely on recursive descent so
+            // internalization over these follows top-down
             TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m_manager););
             svector<expr_bool_pair> sorted_exprs;
             top_sort_expr(n, sorted_exprs);
             TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
-            for (auto & kv : sorted_exprs) internalize(kv.first, kv.second);
+            for (auto & kv : sorted_exprs) {
+                expr* e = kv.first;
+                if (!is_app(e) || 
+                    to_app(e)->get_family_id() == null_family_id || 
+                    to_app(e)->get_family_id() == m_manager.get_basic_family_id()) 
+                    internalize(e, kv.second);
+            }
         }
         SASSERT(m_manager.is_bool(n));
         if (is_gate(m_manager, n)) {