diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index fb8d61e8a..0c876e8bc 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -150,13 +150,6 @@ namespace smt {
 
     literal theory::mk_literal(expr* _e) {
         expr_ref e(_e, m);
-        if (has_quantifiers(e)) {
-            expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m);
-            expr_ref eq(m.mk_eq(fn, e), m);
-            ctx.assert_expr(eq);
-            ctx.internalize_assertions();
-            return mk_literal(fn);
-        }
         bool is_not = m.is_not(_e, _e);
         if (!ctx.e_internalized(_e)) {
             ctx.internalize(_e, is_quantifier(_e));
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 722e3343d..e70e75c8c 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -146,7 +146,17 @@ void theory_user_propagator::propagate() {
                 lit.neg();
             for (auto const& [a,b] : m_eqs)
                 m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
-            literal lit = mk_literal(prop.m_conseq);            
+
+            literal lit; 
+            if (has_quantifiers(prop.m_conseq)) {
+                expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m);
+                expr_ref eq(m.mk_eq(fn, prop.m_conseq), m);
+                ctx.assert_expr(eq);
+                ctx.internalize_assertions();
+                lit = mk_literal(fn);
+            }
+            else 
+                lit = mk_literal(prop.m_conseq);            
             ctx.mark_as_relevant(lit);
             m_lits.push_back(lit);
             ctx.mk_th_lemma(get_id(), m_lits);