diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index cc51f6408..b4f326d5b 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -18,9 +18,6 @@ Notes:
 
 
 #include "ast/euf/euf_egraph.h"
-#include "ast/euf/euf_bv_plugin.h"
-#include "ast/euf/euf_arith_plugin.h"
-#include "ast/euf/euf_specrel_plugin.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_translation.h"
 
@@ -123,10 +120,8 @@ namespace euf {
             n->mark_interpreted();
         if (m_on_make)
             m_on_make(n);
-
-        if (num_args == 0) 
+        if (num_args == 0)
             return n;
-        
         if (m.is_eq(f) && !m.is_iff(f)) {
             n->set_is_equality();
             reinsert_equality(n);
@@ -474,7 +469,7 @@ namespace euf {
 
         if (!n1->cgc_enabled() && !n2->cgc_enabled())
             return;
-        
+        SASSERT(n1->get_sort() == n2->get_sort());
         enode* r1 = n1->get_root();
         enode* r2 = n2->get_root();
         if (r1 == r2)
@@ -484,7 +479,6 @@ namespace euf {
         IF_VERBOSE(20, j.display(verbose_stream() << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";);
         force_push();
         SASSERT(m_num_scopes == 0);
-        SASSERT(n1->get_sort() == n2->get_sort());
         ++m_stats.m_num_merge;
         if (r1->interpreted() && r2->interpreted()) {
             set_conflict(n1, n2, j);
@@ -510,7 +504,7 @@ namespace euf {
         std::swap(r1->m_next, r2->m_next);
         r2->inc_class_size(r1->class_size());   
         r2->set_is_shared(l_undef);
-        merge_th_eq(r1, r2, j);
+        merge_th_eq(r1, r2);
         reinsert_parents(r1, r2);
         if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
             add_literal(n1, r2);
@@ -521,7 +515,6 @@ namespace euf {
 
         for (auto& cb : m_on_merge)
             cb(r2, r1);
-    
     }
 
     void egraph::remove_parents(enode* r) {
@@ -568,7 +561,7 @@ namespace euf {
         }
     }
 
-    void egraph::merge_th_eq(enode* n, enode* root, justification j) {
+    void egraph::merge_th_eq(enode* n, enode* root) {
         SASSERT(n != root);
         for (auto const& iv : enode_th_vars(n)) {
             theory_id id = iv.get_id();
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 7f63c35ee..0f5f220dc 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -234,7 +234,7 @@ namespace euf {
         void force_push();
         void set_conflict(enode* n1, enode* n2, justification j);
         void merge(enode* n1, enode* n2, justification j);
-        void merge_th_eq(enode* n, enode* root, justification j);
+        void merge_th_eq(enode* n, enode* root);
         void merge_justification(enode* n1, enode* n2, justification j);
         void reinsert_parents(enode* r1, enode* r2);
         void remove_parents(enode* r);
@@ -280,8 +280,6 @@ namespace euf {
         void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }        
         void new_diseq(enode* n);
 
-        bool can_propagate() const { return !m_to_merge.empty(); }
-
         /**
            \brief propagate set of merges. 
            This call may detect an inconsistency. Then inconsistent() is true.
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index ba462b811..21b1b7f8c 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -387,7 +387,7 @@ namespace bv {
             for (unsigned i = 0; i < c.m_num_literals; ++i)
                 r.push_back(c.m_literals[i]);
             for (unsigned i = 0; i < c.m_num_eqs; ++i)
-                ctx.add_antecedent(probing, c.m_eqs[i].first, c.m_eqs[i].second);            
+                ctx.add_eq_antecedent(probing, c.m_eqs[i].first, c.m_eqs[i].second);            
             break;
         }
         default:
diff --git a/src/util/dependency.h b/src/util/dependency.h
index dc17826d6..6094cc555 100644
--- a/src/util/dependency.h
+++ b/src/util/dependency.h
@@ -341,15 +341,6 @@ public:
     void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) const {
         return m_dep_manager.linearize(d, vs);
     }    
-
-    static vector<value, false> const& s_linearize(dependency* d, vector<value, false>& vs) {
-        dep_manager::s_linearize(d, vs);
-        return vs;
-    }
-
-    void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) {
-        return m_dep_manager.linearize(d, vs);
-    }    
     
     void reset() {
         m_allocator.reset();