diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index 03f9f8ed1..7e9b20af7 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -38,11 +38,18 @@ namespace euf {
         }
     }
 
+    /**
+     * Add a root clause. Root clauses must all be satisfied by the 
+     * final assignment. If a clause is added above search level it
+     * is subject to removal on backtracking. These clauses are therefore
+     * not tracked.
+     */
     void solver::add_root(unsigned n, sat::literal const* lits) {
         if (!relevancy_enabled())
             return;
         ensure_dual_solver();
-        m_dual_solver->add_root(n, lits);
+        if (s().at_search_lvl())
+            m_dual_solver->add_root(n, lits);
     }
 
     void solver::add_aux(unsigned n, sat::literal const* lits) {
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index f74ce4778..524c3f1c6 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -62,7 +62,7 @@ namespace q {
         if (l.sign() == is_forall(e)) {
             sat::literal lit = skolemize(q);
             add_clause(~l, lit);
-            ctx.add_aux(~l, lit);
+            ctx.add_root(~l, lit);
         }
         else {
             ctx.push_vec(m_universal, l);