diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index cba15a0f33..3ecaf4e2bb 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -152,8 +152,12 @@ namespace smt {
         expr_ref e(_e, m);
         bool is_not = m.is_not(_e, _e);
         if (!ctx.e_internalized(_e)) {
-            auto n = ctx.non_ground_internalize(_e);
-            _e = n->get_expr();            
+            if (is_quantifier(_e))
+                ctx.internalize(_e, true);
+            else {
+                auto n = ctx.non_ground_internalize(_e);
+                _e = n->get_expr();
+            }
         }
         literal lit = ctx.get_literal(_e);
         ctx.mark_as_relevant(lit);