diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 2caf0eb75..eebb4a721 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -61,8 +61,11 @@ namespace q {
             return;
         }
 
-        if (l.sign() == is_forall(e)) 
-            add_clause(~l, skolemize(q));
+        if (l.sign() == is_forall(e)) {
+            sat::literal lit = skolemize(q);
+            add_clause(~l, lit);
+            ctx.add_root(~l, lit);
+        }
         else {
             ctx.push_vec(m_universal, l);
             if (ctx.get_config().m_ematching)