diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index f6cc881b5..74bb182e8 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -266,6 +266,11 @@ namespace sat {
         //
         // -----------------------
         void add_clause(unsigned num_lits, literal * lits, sat::status st) override { mk_clause(num_lits, lits, st); }
+        void add_clause(literal l1, literal l2, status st) {
+            literal lits[2] = { l1, l2 };
+            add_clause(2, lits, st);
+        }
+        void add_clause(literal lit, status st) { literal lits[1] = { lit }; add_clause(1, lits, st); }
         bool_var add_var(bool ext) override { return mk_var(ext, true); }
 
         bool_var mk_var(bool ext = false, bool dvar = true);
diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h
index ca66003cb..407deae5c 100644
--- a/src/sat/sat_solver_core.h
+++ b/src/sat/sat_solver_core.h
@@ -35,10 +35,7 @@ namespace sat {
 
         // add clauses
         virtual void add_clause(unsigned n, literal* lits, status st) = 0;
-        void add_clause(literal l1, literal l2, status st) {
-            literal lits[2] = {l1, l2};
-            add_clause(2, lits, st);
-        }
+        
         void add_clause(literal l1, literal l2, literal l3, status st) {
             literal lits[3] = {l1, l2, l3};
             add_clause(3, lits, st);
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 8a7d16b31..51f342fe1 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -220,8 +220,8 @@ namespace euf {
                     lits.push_back(lit);
                 }
             }
-            s().mk_clause(lits, st);
             add_root(lits);
+            s().mk_clause(lits, st);
         }
         else {
             // g(f(x_i)) = x_i
@@ -239,14 +239,13 @@ namespace euf {
                 expr_ref gapp(m.mk_app(g, fapp.get()), m);
                 expr_ref eq = mk_eq(gapp, arg);
                 sat::literal lit = mk_literal(eq);
-                s().add_clause(1, &lit, st);
+                s().add_clause(lit, st);
                 eqs.push_back(mk_eq(fapp, a));
             }
             pb_util pb(m);
             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);
-            add_root(lit);
+            s().add_clause(lit, st);
         }
     }
 
@@ -262,8 +261,7 @@ namespace euf {
                 for (unsigned j = i + 1; j < sz; ++j) {
                     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);
-                    add_root(1, &lit);
+                    s().add_clause(lit, st);
                 }
             }
         }
@@ -280,8 +278,7 @@ namespace euf {
                 n->mark_interpreted();
                 expr_ref eq = mk_eq(fapp, fresh);
                 sat::literal lit = mk_literal(eq);
-                s().add_clause(1, &lit, st);
-                add_root(1, &lit);
+                s().add_clause(lit, st);
             }
         }
     }
@@ -294,18 +291,16 @@ namespace euf {
             expr_ref eq_th = mk_eq(e, th);
             sat::literal lit_th = mk_literal(eq_th);
             if (th == el) {
-                s().add_clause(1, &lit_th, st);
+                s().add_clause(lit_th, st);
             }
             else {
                 sat::literal lit_c = mk_literal(c);
                 expr_ref eq_el = mk_eq(e, el);
                 sat::literal lit_el = mk_literal(eq_el);
-                literal lits1[2] = { ~lit_c,  lit_th };
-                literal lits2[2] = { lit_c, lit_el };
-                s().add_clause(2, lits1, st);
-                s().add_clause(2, lits2, st);
-                add_root(2, lits1);
-                add_root(2, lits2);
+                add_root(~lit_c, lit_th);
+                add_root(lit_c, lit_el);
+                s().add_clause(~lit_c, lit_th, st);
+                s().add_clause(lit_c, lit_el, st);
             }
         }
         else if (m.is_distinct(e)) {
@@ -320,12 +315,10 @@ namespace euf {
             expr_ref fml(m.mk_or(eqs), m);
             sat::literal dist(si.to_bool_var(e), false);
             sat::literal some_eq = si.internalize(fml, m_is_redundant);
-            sat::literal lits1[2] = { ~dist, ~some_eq };
-            sat::literal lits2[2] = { dist, some_eq };
-            s().add_clause(2, lits1, st);
-            s().add_clause(2, lits2, st);
-            add_root(2, lits1);
-            add_root(2, lits2);
+            add_root(~dist, ~some_eq);
+            add_root(dist, some_eq);
+            s().add_clause(~dist, ~some_eq, st);
+            s().add_clause(dist, some_eq, st);
         }
         else if (m.is_eq(e, th, el) && !m.is_iff(e)) {
             sat::literal lit1 = expr2literal(e);
@@ -334,12 +327,10 @@ namespace euf {
             enode* n2 = m_egraph.find(e2);
             if (n2) {
                 sat::literal lit2 = expr2literal(e2);
-                sat::literal lits1[2] = { ~lit1, lit2 };
-                sat::literal lits2[2] = { lit1, ~lit2 };
-                s().add_clause(2, lits1, st);
-                s().add_clause(2, lits2, st);
-                add_root(2, lits1);
-                add_root(2, lits2);
+                add_root(~lit1, lit2);
+                add_root(lit1, ~lit2);
+                s().add_clause(~lit1, lit2, st);
+                s().add_clause(lit1, ~lit2, st);
             }
         }
     }
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 1913e1bd3..859c0640c 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -377,6 +377,7 @@ namespace euf {
         void add_root(unsigned n, sat::literal const* lits) { m_relevancy.add_root(n, lits); }
         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 lit1, sat::literal lit2) { sat::literal lits[2] = { lit1, lit2, }; 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) { m_relevancy.add_def(n, lits); }
         void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); }