diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index 1076acc30..8fef8b316 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -124,7 +124,7 @@ namespace array {
             mk_var(n);
         for (auto* arg : euf::enode_args(n))
             ensure_var(arg);  
-        if (ctx.is_relevant(n))
+        if (ctx.is_relevant(n) || !ctx.relevancy().enabled())
             relevant_eh(n);
         return true;
     }
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 2fec734df..77115b441 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -427,7 +427,6 @@ namespace bv {
         expr_ref sum(m_autil.mk_add(sz, args.data()), m);
         sat::literal lit = eq_internalize(n, sum);
 	add_unit(lit);
-	ctx.add_root(lit);
     }
 
     void solver::internalize_int2bv(app* n) {
@@ -457,7 +456,6 @@ namespace bv {
         rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
 	sat::literal eq_lit = eq_internalize(lhs, rhs);
 	add_unit(eq_lit);
-	ctx.add_root(eq_lit);
        
         expr_ref_vector n_bits(m);
         get_bits(n_enode, n_bits);
@@ -470,7 +468,6 @@ namespace bv {
             lhs = n_bits.get(i);
 	    eq_lit = eq_internalize(lhs, rhs);
 	    add_unit(eq_lit);
-	    ctx.add_root(eq_lit);
         }
     }
 
@@ -536,7 +533,6 @@ namespace bv {
         if (p.hi_div0()) {
             eq_lit = eq_internalize(n, ibin(arg1, arg2));
 	    add_unit(eq_lit);
-	    ctx.add_root(eq_lit);
 	}
 	else {
 	    unsigned sz = bv.get_bv_size(n);
@@ -654,7 +650,6 @@ namespace bv {
         mk_bits(get_th_var(e));
 	sat::literal eq_lit = eq_internalize(e, r);
         add_unit(eq_lit);
-	ctx.add_root(eq_lit);
     }
 
     void solver::internalize_bit2bool(app* n) {
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 90a268661..6079002a5 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -162,10 +162,8 @@ namespace euf {
             sat::literal lit2 = literal(v, false);
             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_aux(~lit, lit2);
-                add_aux(lit, ~lit2);
-            }
+            add_aux(~lit, lit2);
+            add_aux(lit, ~lit2);
             lit = lit2;
         }
 
@@ -225,8 +223,7 @@ namespace euf {
                 }
             }
             s().mk_clause(lits, st);
-            if (relevancy_enabled())
-                add_root(lits);
+            add_root(lits);
         }
         else {
             // g(f(x_i)) = x_i
@@ -251,8 +248,7 @@ namespace euf {
             expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m);
             sat::literal lit = si.internalize(at_least2, m_is_redundant);
             s().mk_clause(1, &lit, st);
-            if (relevancy_enabled())
-                add_root(1, &lit);
+            add_root(1, &lit);
         }
     }
 
@@ -269,8 +265,7 @@ namespace euf {
                     expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
                     sat::literal lit = ~mk_literal(eq);
                     s().add_clause(1, &lit, st);
-                    if (relevancy_enabled())
-                        add_root(1, &lit);
+                    add_root(1, &lit);
                 }
             }
         }
@@ -288,8 +283,7 @@ namespace euf {
                 expr_ref eq = mk_eq(fapp, fresh);
                 sat::literal lit = mk_literal(eq);
                 s().add_clause(1, &lit, st);
-                if (relevancy_enabled())
-                    add_root(1, &lit);
+                add_root(1, &lit);
             }
         }
     }
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index a7a2d67d7..20e65b8d6 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -71,7 +71,6 @@ namespace q {
             euf::solver::scoped_generation sg(ctx, generation + 1);
             sat::literal lit = ctx.mk_literal(fml);
             m_qs.add_clause(~qlit, ~lit);
-            ctx.add_root(~qlit, ~lit);
         }
         m_instantiations.reset();
         return result;
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 148383c2b..6ef4012af 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -44,19 +44,16 @@ namespace q {
         if (l.sign() == is_forall(e)) {
             sat::literal lit = skolemize(q);
             add_clause(~l, lit);
-            ctx.add_root(~l, lit);
         }
         else if (expand(q)) {
             for (expr* e : m_expanded) {
                 sat::literal lit = ctx.internalize(e, l.sign(), false, false);
                 add_clause(~l, lit);
-                ctx.add_root(~l, lit);
             }
         }
         else if (is_ground(q->get_expr())) {
             auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false);
             add_clause(~l, lit);
-            ctx.add_root(~l, lit);
         }
         else {
             ctx.push_vec(m_universal, l);
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index 06efccaf0..f72ff601a 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -132,6 +132,7 @@ namespace euf {
     bool th_euf_solver::add_unit(sat::literal lit) {
         bool was_true = is_true(lit);
         ctx.s().add_clause(1, &lit, mk_status());
+        ctx.add_root(lit);
         return !was_true;
     }
 
@@ -143,32 +144,27 @@ namespace euf {
         return is_new;
     }
 
-    bool th_euf_solver::add_clause(sat::literal a, sat::literal b) {
-        bool was_true = is_true(a, b);
+    bool th_euf_solver::add_clause(sat::literal a, sat::literal b) {      
         sat::literal lits[2] = { a, b };
-        ctx.s().add_clause(2, lits, mk_status());
-        return !was_true;
+        return add_clause(2, lits);
     }
 
-    bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {
-        bool was_true = is_true(a, b, c);
+    bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {      
         sat::literal lits[3] = { a, b, c };
-        ctx.s().add_clause(3, lits, mk_status());
-        return !was_true;
+        return add_clause(3, lits);
     }
 
     bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) {
-        bool was_true = is_true(a, b, c, d);
         sat::literal lits[4] = { a, b, c, d };
-        ctx.s().add_clause(4, lits, mk_status());
-        return !was_true;
+        return add_clause(4, lits);
     }
 
-    bool th_euf_solver::add_clause(sat::literal_vector const& lits) {
+    bool th_euf_solver::add_clause(unsigned n, sat::literal* lits) {
         bool was_true = false;
-        for (auto lit : lits)
-            was_true |= is_true(lit);
-        s().add_clause(lits.size(), lits.data(), mk_status());
+        for (unsigned i = 0; i < n; ++i)       
+            was_true |= is_true(lits[i]);
+        ctx.add_root(n, lits);
+        s().add_clause(n, lits, mk_status());
         return !was_true;
     }
 
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index fecb745c5..16138441c 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -141,7 +141,8 @@ namespace euf {
         bool add_clause(sat::literal a, sat::literal b);
         bool add_clause(sat::literal a, sat::literal b, sat::literal c);
         bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d);
-        bool add_clause(sat::literal_vector const& lits);
+        bool add_clause(sat::literal_vector const& lits) { return add_clause(lits.size(), lits.data()); }
+        bool add_clause(unsigned n, sat::literal* lits);
         void add_equiv(sat::literal a, sat::literal b);
         void add_equiv_and(sat::literal a, sat::literal_vector const& bs);