diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index fbe54c8fe1f..080cd4a88d7 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -591,6 +591,7 @@ namespace euf {
             else 
                 lit = si.internalize(e, true);
             VERIFY(lit.var() == v);
+            
             attach_lit(lit, e);            
         }
         
@@ -654,10 +655,10 @@ namespace euf {
             break;
         }
         case OP_TRUE:
-            add_root(lit);
+            add_aux(lit);
             break;
         case OP_FALSE:
-            add_root(~lit);
+            add_aux(~lit);
             break;
         case OP_ITE: {
             auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index db928259c9c..f34819da399 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -369,6 +369,7 @@ namespace euf {
         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 lits[1] = { a }; add_aux(1, lits); }
         void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } 
         void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); }
         void track_relevancy(sat::bool_var v);