diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 037020a2e..ad88f839f 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -36,10 +36,8 @@ namespace euf {
         }
         m_expr2enode.setx(f->get_id(), n, nullptr);
         push_node(n);
-        for (unsigned i = 0; i < num_args; ++i) {
-            set_cgc_enabled(args[i], true);
-            set_merge_tf_enabled(args[i], true);            
-        }
+        for (unsigned i = 0; i < num_args; ++i) 
+            set_cgc_enabled(args[i], true);                             
         return n;
     }
 
@@ -271,12 +269,6 @@ namespace euf {
         if (enable_merge_tf != n->merge_tf()) {
             n->set_merge_tf(enable_merge_tf);
             m_updates.push_back(update_record(n, update_record::toggle_merge_tf()));
-            if (enable_merge_tf && n->value() != l_undef && !m.is_value(n->get_root()->get_expr())) {
-                expr* b = n->value() == l_true ? m.mk_true() : m.mk_false();
-                enode* tf = find(b);
-                if (tf) 
-                    add_literal(n, tf);
-            }
         }
     }
 
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 3aaafa36c..792ffcf1d 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -474,6 +474,33 @@ namespace euf {
         enode* n = m_egraph.mk(e, m_generation, num, args);
         if (si.is_bool_op(e)) 
             m_egraph.set_cgc_enabled(n, false);
+
+        //
+        // (if p th el) (non-Boolean case) produces clauses 
+        //     (=> p (= (if p th el) th))
+        // and (=> (not p) (= (if p th el) el))
+        // The clauses establish equalities between the ite term and 
+        // the th or el sub-terms.
+        // 
+        if (m.is_ite(e))
+            num = 0;
+
+        //
+        // To track congruences of Boolean children under non-Boolean 
+        // functions set the merge_tf flag to true.
+        //
+        for (unsigned i = 0; i < num; ++i) {
+            if (!m.is_bool(args[i]->get_sort()))
+                continue;
+            bool was_enabled = args[i]->merge_tf();
+            m_egraph.set_merge_tf_enabled(args[i], true);
+            if (!was_enabled && n->value() != l_undef && !m.is_value(n->get_root()->get_expr())) {
+                if (n->value() == l_true)
+                    m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
+                else
+                    m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var())));
+            }
+        }
         return n;
     }
 
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 5b09e6a46..675ec1500 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -146,7 +146,6 @@ namespace euf {
 
         constraint* m_conflict = nullptr;
         constraint* m_eq = nullptr;
-        constraint* m_lit = nullptr;
 
         // proofs 
         bool                             m_proof_initialized = false;
@@ -266,7 +265,6 @@ namespace euf {
         ~solver() override {
             if (m_conflict) dealloc(sat::constraint_base::mem2base_ptr(m_conflict));
             if (m_eq) dealloc(sat::constraint_base::mem2base_ptr(m_eq));
-            if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
             m_trail.reset();
         }