diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index caf12235c..a7476bc5d 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -140,8 +140,8 @@ namespace euf {
             s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
             s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
             if (relevancy_enabled()) {
-                add_root(~lit, lit2);
-                add_root(lit, ~lit2);
+                add_aux(~lit, lit2);
+                add_aux(lit, ~lit2);
             }
             lit = lit2;
         }
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index b114e844f..af670297c 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -50,7 +50,7 @@ namespace q {
             }
             return;
         }
-        if (exp.size() > 1 && is_exists(q) /* && l.sign() */) {
+        if (exp.size() > 1 && is_exists(q) && l.sign()) {
             sat::literal_vector lits;
             lits.push_back(~l);
             for (expr* e : exp)