diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index f5c05cea9..03f9f8ed1 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -39,11 +39,15 @@ namespace euf {
     }
 
     void solver::add_root(unsigned n, sat::literal const* lits) {
+        if (!relevancy_enabled())
+            return;
         ensure_dual_solver();
         m_dual_solver->add_root(n, lits);
     }
 
     void solver::add_aux(unsigned n, sat::literal const* lits) {
+        if (!relevancy_enabled())
+            return;
         ensure_dual_solver();
         m_dual_solver->add_aux(n, lits);
     }
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 73c44649c..cf8b9766e 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -361,6 +361,7 @@ namespace euf {
         void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); }
         void add_root(sat::literal lit) { add_root(1, &lit); }
         void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); }
+        void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); }
         void add_aux(unsigned n, sat::literal const* lits);
         void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } 
         void track_relevancy(sat::bool_var v);
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index af670297c..f74ce4778 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -45,8 +45,7 @@ namespace q {
             for (expr* e : exp) {
                 sat::literal lit = ctx.internalize(e, l.sign(), false, false); 
                 add_clause(~l, lit);                    
-                if (ctx.relevancy_enabled())
-                    ctx.add_root(~l, lit);
+                ctx.add_aux(~l, lit);
             }
             return;
         }
@@ -56,14 +55,14 @@ namespace q {
             for (expr* e : exp)
                 lits.push_back(ctx.internalize(e, l.sign(), false, false));
             add_clause(lits);
-            ctx.add_root(lits);
+            ctx.add_aux(lits);
             return;
         }
 
         if (l.sign() == is_forall(e)) {
             sat::literal lit = skolemize(q);
             add_clause(~l, lit);
-            ctx.add_root(~l, lit);
+            ctx.add_aux(~l, lit);
         }
         else {
             ctx.push_vec(m_universal, l);
diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index b392254a1..6676603bc 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -81,9 +81,9 @@ namespace sat {
         return literal(m_var2ext[lit.var()], lit.sign());
     }
 
-    void dual_solver::add_root(unsigned sz, literal const* clause) {
-        TRACE("dual", tout << "root: " << literal_vector(sz, clause) << "\n";);
+    void dual_solver::add_root(unsigned sz, literal const* clause) {        
         if (sz == 1) {
+            TRACE("dual", tout << "unit: " << clause[0] << "\n";);
             m_units.push_back(clause[0]);
             return;
         }
@@ -91,6 +91,7 @@ namespace sat {
         for (unsigned i = 0; i < sz; ++i)
             m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
         m_roots.push_back(~root);
+        TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";);
     }
 
     void dual_solver::add_aux(unsigned sz, literal const* clause) {