diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index b2c7edc34..a2c2886e0 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -460,6 +460,7 @@ func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* dom
         m_manager->raise_exception("set-has-size takes two arguments");
         return nullptr;
     }    
+    m_manager->raise_exception("set-has-size is not supported");
     // domain[0] is a Boolean array,
     // domain[1] is Int
     arith_util arith(*m_manager);
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 0045d7efa..595a0f644 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -22,6 +22,7 @@ Author:
 
 namespace euf {
 
+
     void egraph::undo_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
         enode* r2 = r1->get_root();
         r2->dec_class_size(r1->class_size());
@@ -113,6 +114,7 @@ namespace euf {
 
     egraph::egraph(ast_manager& m) : m(m), m_table(m), m_exprs(m) {
         m_tmp_eq = enode::mk_tmp(m_region, 2);
+        // m_updates.reserve(10000, update_record(nullptr));
     }
 
     egraph::~egraph() {
@@ -143,14 +145,15 @@ namespace euf {
         if (is_eq) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits;
     }
 
-    void egraph::new_diseq(enode* n1) {
-        SASSERT(n1->is_equality());
-        enode* arg1 = n1->get_arg(0), * arg2 = n1->get_arg(1);
+    void egraph::new_diseq(enode* n) {
+        SASSERT(n->is_equality());
+        SASSERT(n->value() == l_false);
+        enode* arg1 = n->get_arg(0), * arg2 = n->get_arg(1);
         enode* r1 = arg1->get_root();
         enode* r2 = arg2->get_root();
         TRACE("euf", tout << "new-diseq:  " << mk_pp(r1->get_expr(), m) << " " << mk_pp(r2->get_expr(), m) << ": " << r1->has_th_vars() << " " << r2->has_th_vars() << "\n";);
         if (r1 == r2) {
-            add_literal(n1, true);
+            add_literal(n, true);
             return;
         }
         if (!r1->has_th_vars())
@@ -163,7 +166,7 @@ namespace euf {
                 return;
             theory_var v1 = arg1->get_closest_th_var(id);
             theory_var v2 = arg2->get_closest_th_var(id);
-            add_th_diseq(id, v1, v2, n1->get_expr());
+            add_th_diseq(id, v1, v2, n->get_expr());
             return;
         }
         for (auto p : euf::enode_th_vars(r1)) {
@@ -171,7 +174,7 @@ namespace euf {
                 continue;
             for (auto q : euf::enode_th_vars(r2))
                 if (p.get_id() == q.get_id()) 
-                    add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n1->get_expr());
+                    add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n->get_expr());
         }
     }
 
@@ -250,9 +253,9 @@ namespace euf {
         }
     }
 
-    void egraph::set_value(enode* n, lbool value) {
+    void egraph::set_value(enode* n, lbool value) {        
         force_push();
-        VERIFY(n->value() == l_undef);
+        SASSERT(n->value() == l_undef);
         n->set_value(value);
         m_updates.push_back(update_record(n, update_record::value_assignment()));
     }
@@ -331,9 +334,8 @@ namespace euf {
     }
 
     void egraph::merge(enode* n1, enode* n2, justification j) {
-        if (!n1->merge_enabled() && !n2->merge_enabled()) {
-            return;
-        }
+        if (!n1->merge_enabled() && !n2->merge_enabled()) 
+            return;        
         SASSERT(m.get_sort(n1->get_expr()) == m.get_sort(n2->get_expr()));
         enode* r1 = n1->get_root();
         enode* r2 = n2->get_root();
@@ -357,7 +359,7 @@ namespace euf {
         if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr()))) {
             add_literal(n1, false);
         }
-        if (n1->is_equality() && r2->value() == l_false)
+        if (n1->is_equality() && n1->value() == l_false)
             new_diseq(n1);       
         unsigned num_merge = 0, num_eqs = 0;
         for (enode* p : enode_parents(n1)) {
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 164bc4597..44b77ded3 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -207,7 +207,7 @@ namespace euf {
            \brief merge nodes, all effects are deferred to the propagation step.
          */
         void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }        
-        void new_diseq(enode* n1);
+        void new_diseq(enode* n);
 
 
         /**
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 7b1411edb..49b577bf9 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -285,7 +285,8 @@ bool cmd_context::contains_func_decl(symbol const& s, unsigned n, sort* const* d
 }
 
 bool cmd_context::contains_macro(symbol const& s) const {
-    return m_macros.contains(s);
+    macro_decls decls;
+    return m_macros.find(s, decls) && !decls.empty();
 }
 
 bool cmd_context::contains_macro(symbol const& s, func_decl* f) const {
@@ -851,6 +852,7 @@ void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain,
     insert_macro(s, arity, domain, t);
     if (!m_global_decls) {
         m_macros_stack.push_back(s);
+        
     }
 }
 
@@ -890,6 +892,8 @@ void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domai
     fs.insert(m(), fn);
     VERIFY(fn->get_range() == m().get_sort(t));
     m_mc0->add(fn, t);
+    if (!m_global_decls)
+        m_func_decls_stack.push_back(sf_pair(s, fn));
 }
 
 void cmd_context::model_del(func_decl* f) {
@@ -1424,10 +1428,8 @@ void cmd_context::restore_macros(unsigned old_sz) {
     SASSERT(old_sz <= m_macros_stack.size());
     svector<symbol>::iterator it  = m_macros_stack.begin() + old_sz;
     svector<symbol>::iterator end = m_macros_stack.end();
-    for (; it != end; ++it) {
-        symbol const & s = *it;
-        erase_macro(s);
-    }
+    for (; it != end; ++it) 
+        erase_macro(*it);    
     m_macros_stack.shrink(old_sz);
 }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 6b21d3836..6a67cf0b4 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -81,6 +81,7 @@ public:
     macro_decls() { m_decls = nullptr; }
     void finalize(ast_manager& m);
     bool insert(ast_manager& m, unsigned arity, sort *const* domain, expr* body);
+    bool empty() const { return !m_decls || m_decls->empty(); }
     expr* find(unsigned arity, sort *const* domain) const;
     void erase_last(ast_manager& m);
     vector<macro_decl>::iterator begin() const { return m_decls->begin(); }
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 1c243867d..69f9fe7b8 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -218,10 +218,12 @@ namespace sat {
 
     void elim_eqs::save_elim(literal_vector const & roots, bool_var_vector const & to_elim) {
         model_converter & mc = m_solver.m_mc;
+
         for (bool_var v : to_elim) {
             literal  l(v, false);
             literal r  = roots[v];
             SASSERT(v != r.var());
+
             if (m_solver.m_cut_simplifier) m_solver.m_cut_simplifier->set_root(v, r);
             bool set_root = m_solver.set_root(l, r);
             bool root_ok = !m_solver.is_external(v) || set_root;
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index 7ce073975..5a18b2899 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -203,6 +203,7 @@ namespace sat {
                             in_s[l2_idx] = false;
                             literal  l2 = to_literal(l2_idx);
                             bool_var v2 = l2.var();
+
                             if (roots[v2] == null_literal) {
                                 if (l2.sign()) {
                                     roots[v2] = ~r;
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index f3c09ffb7..b79635dda 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -995,6 +995,7 @@ namespace sat {
             literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
             bool empty() const { return m_queue.empty(); }
             void reset() { m_queue.reset(); }
+            unsigned size() const { return m_queue.size(); }
         };
 
         simplifier &      s;
@@ -1589,9 +1590,8 @@ namespace sat {
             SASSERT(!s.is_external(l));
             model_converter::entry& new_entry = m_mc.mk(k, l.var());
             for (literal lit : c) {
-                if (lit != l && process_var(lit.var())) {
-                    m_queue.decreased(~lit);
-                }
+                if (lit != l && process_var(lit.var())) 
+                    m_queue.decreased(~lit);                
             }
             m_mc.insert(new_entry, m_covered_clause);
             m_mc.set_clause(new_entry, c);
@@ -1605,7 +1605,8 @@ namespace sat {
             s.set_learned(l1, l2);
             m_mc.insert(new_entry, m_covered_clause);
             m_mc.set_clause(new_entry, l1, l2);
-            m_queue.decreased(~l2);
+            if (process_var(l2.var()))
+                m_queue.decreased(~l2);
         }
 
         void bca() {
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 16c1471c4..9ce23799e 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -318,24 +318,7 @@ namespace sat {
     }
 
     void solver::set_external(bool_var v) {
-        if (m_external[v]) return;
         m_external[v] = true;
-        if (!m_ext) return;
-        
-        lbool val = value(v);
-
-        switch (val) {
-        case l_true: {
-            m_ext->asserted(literal(v, false));
-            break;
-        }
-        case l_false: {
-            m_ext->asserted(literal(v, true));
-            break;
-        }
-        default:
-            break;
-        }
     }
 
     void solver::set_eliminated(bool_var v, bool f) { 
@@ -347,10 +330,13 @@ namespace sat {
 
     clause* solver::mk_clause(unsigned num_lits, literal * lits, sat::status st) {
         m_model_is_current = false;
+        for (unsigned i = 0; i < num_lits; i++) 
+            VERIFY(!was_eliminated(lits[i]));
+        
         DEBUG_CODE({
                 for (unsigned i = 0; i < num_lits; i++) {
-                    CTRACE("sat", m_eliminated[lits[i].var()], tout << lits[i] << " was eliminated\n";);
-                    SASSERT(m_eliminated[lits[i].var()] == false);
+                    CTRACE("sat", was_eliminated(lits[i]), tout << lits[i] << " was eliminated\n";);
+                    SASSERT(!was_eliminated(lits[i]));
                 }
         });
 
@@ -587,7 +573,7 @@ namespace sat {
         m_stats.m_mk_clause++;
         clause * r = alloc_clause(num_lits, lits, st.is_redundant());
         SASSERT(!st.is_redundant() || r->is_learned());
-        bool reinit = attach_nary_clause(*r);
+        bool reinit = attach_nary_clause(*r, st.is_sat() && st.is_redundant());
         if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r);
         if (st.is_redundant()) {
             m_learned.push_back(r);
@@ -604,11 +590,11 @@ namespace sat {
         return r;
     }
 
-    bool solver::attach_nary_clause(clause & c) {
+    bool solver::attach_nary_clause(clause & c, bool is_asserting) {
         bool reinit = false;
         clause_offset cls_off = cls_allocator().get_offset(&c);
         if (!at_base_lvl()) {
-            if (c.is_learned() && !c.on_reinit_stack()) {
+            if (is_asserting) {
                 unsigned w2_idx = select_learned_watch_lit(c);
                 std::swap(c[1], c[w2_idx]);
             }
@@ -626,7 +612,7 @@ namespace sat {
                     level = std::max(level, lvl(c[i]));
                 }
                 assign(c[1], justification(level, cls_off));
-                reinit = !c.is_learned();
+                reinit |= !c.is_learned();
             }
             else if (value(c[1]) == l_false) {
                 m_stats.m_propagate++;
@@ -635,7 +621,7 @@ namespace sat {
                     level = std::max(level, lvl(c[i]));
                 }
                 assign(c[0], justification(level, cls_off));
-                reinit = !c.is_learned();
+                reinit |= !c.is_learned();
             }
         }
         unsigned some_idx = c.size() >> 1;
@@ -655,7 +641,7 @@ namespace sat {
         if (ENABLE_TERNARY && c.size() == 3)
             reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted());
         else
-            reinit = attach_nary_clause(c);
+            reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
     }
 
     void solver::set_learned(clause& c, bool redundant) {
@@ -1332,16 +1318,18 @@ namespace sat {
                 return l_undef;
             }
 
-            if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
+            log_stats();
+            if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {               
                 m_restart_threshold = m_config.m_burst_search;
                 lbool r = bounded_search();
-                if (r != l_undef)
+                log_stats();
+                if (r != l_undef) 
                     return r;
+                
                 pop_reinit(scope_lvl());
                 m_conflicts_since_restart = 0;
                 m_restart_threshold = m_config.m_restart_initial;
             }
-            log_stats();
             lbool is_sat = l_undef;
             while (is_sat == l_undef && !should_cancel()) {
                 if (inconsistent()) is_sat = resolve_conflict_core();
@@ -1353,6 +1341,7 @@ namespace sat {
                 else if (should_simplify()) do_simplify();
                 else if (!decide()) is_sat = final_check();
             }
+            log_stats();
             return is_sat;
         }
         catch (const abort_solver &) {
@@ -3588,8 +3577,6 @@ namespace sat {
         if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n");
         for (unsigned i = m_replay_assign.size(); i-- > 0; ) {
             literal lit = m_replay_assign[i];
-            if (m_ext && m_external[lit.var()])
-                m_ext->asserted(lit);
             m_trail.push_back(lit);            
         }
         
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index cc400201a..2fb281554 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -290,7 +290,7 @@ namespace sat {
         clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
         bool has_variables_to_reinit(clause const& c) const;
         bool has_variables_to_reinit(literal l1, literal l2) const;
-        bool attach_nary_clause(clause & c);
+        bool attach_nary_clause(clause & c, bool is_asserting);
         void attach_clause(clause & c, bool & reinit);
         void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
         void set_learned(clause& c, bool learned);
diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp
index beee6a558..a788e5cfd 100644
--- a/src/sat/smt/bv_ackerman.cpp
+++ b/src/sat/smt/bv_ackerman.cpp
@@ -41,18 +41,22 @@ namespace bv {
         if (v1 > v2)
             std::swap(v1, v2);
         vv* n = m_tmp_vv;
-        n->v1 = v1;
-        n->v2 = v2;
+        n->set_var(v1, v2);
         vv* other = m_table.insert_if_not_there(n);        
         other->m_count++;
         update_glue(*other);
-        if (other->m_count > m_propagate_high_watermark || other->m_glue == 0)
-            s.s().set_should_simplify();
+
         vv::push_to_front(m_queue, other);
         if (other == n) {
             new_tmp();        
             gc();
         }
+        if (other->m_glue == 0) {
+            remove(other);
+            add_cc(v1, v2);
+        }
+        else if (other->m_count > m_propagate_high_watermark) 
+            s.s().set_should_simplify();
     }
 
     void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) {
@@ -61,17 +65,17 @@ namespace bv {
         if (v1 > v2)
             std::swap(v1, v2);
         vv* n = m_tmp_vv;
-        n->v1 = v1;
-        n->v2 = v2;
+        n->set_var(v1, v2);
         vv* other = m_table.insert_if_not_there(n);
         other->m_count++;
-        if (other->m_count > m_propagate_high_watermark || other->m_glue == 0)
-            s.s().set_should_simplify();
+
         vv::push_to_front(m_queue, other);
         if (other == n) {
             new_tmp();
             gc();
         }
+        if (other->m_count > m_propagate_high_watermark) 
+            s.s().set_should_simplify();
     }
 
     void ackerman::update_glue(vv& v) {
diff --git a/src/sat/smt/bv_ackerman.h b/src/sat/smt/bv_ackerman.h
index cba6e50ad..f6465abc7 100644
--- a/src/sat/smt/bv_ackerman.h
+++ b/src/sat/smt/bv_ackerman.h
@@ -32,6 +32,7 @@ namespace bv {
             unsigned   m_glue{ UINT_MAX };
             vv():v1(euf::null_theory_var), v2(euf::null_theory_var) {}
             vv(euf::theory_var v1, euf::theory_var v2):v1(v1), v2(v2) {}
+            void set_var(euf::theory_var x, euf::theory_var y) { v1 = x; v2 = y; m_count = 0; m_glue = UINT_MAX; }
         };
 
         struct vv_eq {
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index b1d7a5467..df37c8ee7 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -29,9 +29,15 @@ namespace bv {
 
     solver::def_atom& solver::atom::to_def() {
         SASSERT(!is_bit());
+        SASSERT(!is_eq());
         return dynamic_cast<def_atom&>(*this);
     }
 
+    solver::eq_atom& solver::atom::to_eq() {
+        SASSERT(is_eq());
+        return dynamic_cast<eq_atom&>(*this);
+    }
+
     class solver::add_var_pos_trail : public trail<euf::solver> {
         solver::bit_atom* m_atom;
     public:
@@ -43,15 +49,43 @@ namespace bv {
     };
 
     class solver::add_eq_occurs_trail : public trail<euf::solver> {
-        solver::bit_atom* m_atom;
+        bit_atom* m_atom;
     public:
-        add_eq_occurs_trail(solver::bit_atom* a) :m_atom(a) {}
+        add_eq_occurs_trail(bit_atom* a) :m_atom(a) {}
         void undo(euf::solver& euf) override {
             SASSERT(m_atom->m_eqs);
             m_atom->m_eqs = m_atom->m_eqs->m_next;
+            if (m_atom->m_eqs)  
+                m_atom->m_eqs->m_prev = nullptr;
         }
     };    
 
+    class solver::del_eq_occurs_trail : public trail<euf::solver> {
+        bit_atom* m_atom;
+        eq_occurs* m_node;
+    public:
+        del_eq_occurs_trail(bit_atom* a, eq_occurs* n) : m_atom(a), m_node(n) {}
+        void undo(euf::solver& euf) override {
+            if (m_node->m_next)
+                m_node->m_next->m_prev = m_node;
+            if (m_node->m_prev) 
+                m_node->m_prev->m_next = m_node;
+            else
+                m_atom->m_eqs = m_node;
+        }
+    };
+
+    void solver::del_eq_occurs(bit_atom* a, eq_occurs* occ) {
+        eq_occurs* prev = occ->m_prev;
+        if (prev)
+            prev->m_next = occ->m_next;
+        else
+            a->m_eqs = occ->m_next;
+        if (occ->m_next)
+            occ->m_next->m_prev = prev;
+        ctx.push(del_eq_occurs_trail(a, occ));
+    }
+
     class solver::mk_atom_trail : public trail<euf::solver> {
         solver& th;
         sat::bool_var m_var;
@@ -263,11 +297,24 @@ namespace bv {
         }
     }
 
+    solver::eq_atom* solver::mk_eq_atom(sat::bool_var bv) {
+        atom* a = get_bv2a(bv);
+        if (a)
+            return a->is_eq() ? &a->to_eq() : nullptr;
+        else {
+            eq_atom* b = new (get_region()) eq_atom();
+            insert_bv2a(bv, b);
+            ctx.push(mk_atom_trail(bv, *this));
+            return b;
+        }
+    }
+
+
     void solver::set_bit_eh(theory_var v, literal l, unsigned idx) {
         SASSERT(m_bits[v][idx] == l);
         if (s().value(l) != l_undef && s().lvl(l) == 0) 
             register_true_false_bit(v, idx);
-        else {
+        else if (m_bits[v].size() > 1) {
             bit_atom* b = mk_bit_atom(l.var());
             if (b) {
                 if (b->m_occs)
@@ -551,15 +598,18 @@ namespace bv {
             mk_var(argn);
         }        
         theory_var v_arg = argn->get_th_var(get_id());
-        SASSERT(idx < get_bv_size(v_arg));
+        unsigned arg_sz = get_bv_size(v_arg);
+        SASSERT(idx < arg_sz);
         sat::literal lit = expr2literal(n);
         sat::literal lit0 = m_bits[v_arg][idx];
         if (lit0 == sat::null_literal) {
             m_bits[v_arg][idx] = lit;
-            bit_atom* a = new (get_region()) bit_atom();
-            a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
-            insert_bv2a(lit.var(), a);
-            ctx.push(mk_atom_trail(lit.var(), *this));
+            if (arg_sz > 1) {
+                bit_atom* a = new (get_region()) bit_atom();
+                a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
+                insert_bv2a(lit.var(), a);
+                ctx.push(mk_atom_trail(lit.var(), *this));
+            }
         }
         else if (lit != lit0) {
             add_clause(lit0, ~lit);
@@ -581,24 +631,60 @@ namespace bv {
 
     void solver::eq_internalized(euf::enode* n) {
         SASSERT(m.is_eq(n->get_expr()));
+        sat::literal lit = literal(n->bool_var(), false);
         theory_var v1 = n->get_arg(0)->get_th_var(get_id());
         theory_var v2 = n->get_arg(1)->get_th_var(get_id());
         SASSERT(v1 != euf::null_theory_var);
         SASSERT(v2 != euf::null_theory_var);
+        
+#if 0
+        if (!n->is_attached_to(get_id()))
+            mk_var(n);
+#endif   
+        
         unsigned sz = m_bits[v1].size();
+        if (sz == 1) {
+            literal bit1 = m_bits[v1][0];
+            literal bit2 = m_bits[v2][0];
+            add_clause(~lit, ~bit1, bit2);
+            add_clause(~lit, ~bit2, bit1);
+            add_clause(~bit1, ~bit2, lit);
+            add_clause(bit2, bit1, lit);
+            return;
+        }
         for (unsigned i = 0; i < sz; ++i) {
-            eq_internalized(m_bits[v1][i].var(), i, v1, v2, n);
-            eq_internalized(m_bits[v2][i].var(), i, v2, v1, n);
+            literal bit1 = m_bits[v1][i];
+            literal bit2 = m_bits[v2][i];
+            lbool val1 = s().value(bit1);
+            lbool val2 = s().value(bit2);
+            if (val1 != l_undef)
+                eq_internalized(bit2.var(), bit1.var(), i, v2, v1, lit, n);
+            else if (val2 != l_undef)
+                eq_internalized(bit1.var(), bit2.var(), i, v1, v2, lit, n);
+            else if ((s().rand()() % 2) == 0)
+                eq_internalized(bit2.var(), bit1.var(), i, v2, v1, lit, n);
+            else 
+                eq_internalized(bit1.var(), bit2.var(), i, v1, v2, lit, n);
         }
     }
 
-    void solver::eq_internalized(sat::bool_var b, unsigned idx, theory_var v1, theory_var v2, euf::enode* n) {
-        bit_atom* a = mk_bit_atom(b);
+    void solver::eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, literal lit, euf::enode* n) {
+        bit_atom* a = mk_bit_atom(b1);
+//        eq_atom* b = mk_eq_atom(lit.var());
         if (a) {
             if (!a->is_fresh()) 
-                ctx.push(add_eq_occurs_trail(a));
-            a->m_eqs = new (get_region()) eq_occurs(idx, v1, v2, expr2literal(n->get_expr()), n, a->m_eqs);
-        }
+                ctx.push(add_eq_occurs_trail(a));            
+            auto* next = a->m_eqs;
+            a->m_eqs = new (get_region()) eq_occurs(b1, b2, idx, v1, v2, lit, n, next);
+            if (next)
+                next->m_prev = a->m_eqs;
+#if 0
+            if (b) {
+                b->m_eqs.push_back(std::make_pair(a, a->m_eqs));
+                ctx.push(push_back_vector<euf::solver, svector<std::pair<bit_atom*,eq_occurs*>>>(b->m_eqs));
+            }
+#endif
+        }        
     }
 
     void solver::assert_ackerman(theory_var v1, theory_var v2) {
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index aa5295d30..12b669200 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -77,7 +77,7 @@ namespace bv {
         else if (var2enode(v1)->get_root() != var2enode(v2)->get_root()) {
             SASSERT(get_bv_size(v1) == get_bv_size(v2));
             TRACE("bv", tout << "detected equality: v" << v1 << " = v" << v2 << "\n" << pp(v1) << pp(v2););
-            m_stats.m_num_th2core_eq++;
+            m_stats.m_num_bit2eq++;
             add_fixed_eq(v1, v2);
             ctx.propagate(var2enode(v1), var2enode(v2), mk_bit2eq_justification(v1, v2));
         }
@@ -146,9 +146,6 @@ namespace bv {
        \brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom.
     */
     void solver::mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
-        if (!get_config().m_bv_eq_axioms)
-            return;
-
         SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
         TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2););
         m_stats.m_num_diseq_static++;
@@ -194,8 +191,10 @@ namespace bv {
     void solver::new_eq_eh(euf::th_eq const& eq) {
         force_push();
         TRACE("bv", tout << "new eq " << mk_bounded_pp(var2expr(eq.v1()), m) << " == " << mk_bounded_pp(var2expr(eq.v2()), m) << "\n";);
-        if (is_bv(eq.v1()))
+        if (is_bv(eq.v1())) {
             m_find.merge(eq.v1(), eq.v2());
+            VERIFY(eq.is_eq());
+        }
     }
 
     void solver::new_diseq_eh(euf::th_eq const& ne) {
@@ -207,6 +206,8 @@ namespace bv {
         
         TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
         unsigned sz = m_bits[v1].size();
+        if (sz == 1)
+            return;
         unsigned num_undef = 0;
         int undef_idx = 0;
         for (unsigned i = 0; i < sz; ++i) {
@@ -245,7 +246,7 @@ namespace bv {
             SASSERT(s().value(b) != l_undef);
             if (s().value(b) == l_true)
                 consequent.neg();
-            ++m_stats.m_num_nbit2core;
+            ++m_stats.m_num_ne2bit;
             s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent));
         }
         else if (s().at_search_lvl()) {
@@ -387,6 +388,11 @@ namespace bv {
             force_push();
             m_prop_queue.push_back(propagation_item(&a->to_bit()));
         }
+        else if (a && a->is_eq()) {
+            for (auto p : a->to_eq().m_eqs) {
+                del_eq_occurs(p.first, p.second);
+            }
+        }
     }
 
     bool solver::unit_propagate() {
@@ -397,10 +403,21 @@ namespace bv {
         for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
             auto const p = m_prop_queue[m_prop_queue_head];
             if (p.m_atom) {
-                for (auto vp : *p.m_atom)
-                    propagate_bits(vp);
-                for (auto const& eq : p.m_atom->eqs())
-                    propagate_eq_occurs(eq);
+                unsigned num_atoms = 0, num_eqs = 0, num_assigned = 0, num_eq_assigned = 0, num_lit_assigned = 0;
+                for (auto vp : *p.m_atom) {
+                    if (propagate_bits(vp))
+                        ++num_assigned;
+                    ++num_atoms;
+                }
+                for (auto const& eq : p.m_atom->eqs()) {
+                    ++num_eqs;
+                    if (s().value(eq.m_literal) != l_undef)
+                        ++num_lit_assigned;
+                    if (propagate_eq_occurs(eq)) {
+                        ++num_eq_assigned;
+                    }
+                }
+                IF_VERBOSE(20, verbose_stream() << "atoms: " << num_atoms << " eqs: " << num_eqs << " atoms-assigned:" << num_assigned << " eqs-assigned: " << num_eq_assigned << " lits: " << num_lit_assigned << "\n");
             }
             else 
                 propagate_bits(p.m_vp);            
@@ -409,20 +426,35 @@ namespace bv {
         return true;
     }
 
-    void solver::propagate_eq_occurs(eq_occurs const& occ) {
+    bool solver::propagate_eq_occurs(eq_occurs const& occ) {
         auto lit = occ.m_literal;
-        if (s().value(lit) != l_undef)
-            return;
-        lbool val1 = s().value(m_bits[occ.m_v1][occ.m_idx]);
-        lbool val2 = s().value(m_bits[occ.m_v2][occ.m_idx]);
+
+        if (s().value(lit) != l_undef) {
+            IF_VERBOSE(20, verbose_stream() << "assigned " << lit << " " << s().value(lit) << "\n");
+            return false;
+        }
+        literal bit1 = m_bits[occ.m_v1][occ.m_idx];
+        literal bit2 = m_bits[occ.m_v2][occ.m_idx];
+        lbool val2 = s().value(bit2);
+        
+        if (val2 == l_undef) {
+            IF_VERBOSE(20, verbose_stream() << "add " << occ.m_bv2 << " " << occ.m_v2 << "\n");
+            eq_internalized(occ.m_bv2, occ.m_bv1, occ.m_idx, occ.m_v2, occ.m_v1, occ.m_literal, occ.m_node);
+            return false;
+        }
+        lbool val1 = s().value(bit1);
         SASSERT(val1 != l_undef);
         if (val1 != val2 && val2 != l_undef) {
-            ++m_stats.m_num_th2core_diseq;
+            ++m_stats.m_num_bit2ne;
+            IF_VERBOSE(20, verbose_stream() << "assign " << ~lit << "\n");
             s().assign(~lit, mk_bit2ne_justification(occ.m_idx, ~lit));
+            return true;
         }
+        IF_VERBOSE(20, verbose_stream() << "eq " << lit << "\n");
+        return false;
     }
 
-    void solver::propagate_bits(var_pos entry) {
+    bool solver::propagate_bits(var_pos entry) {
         theory_var v1 = entry.first;
         unsigned idx = entry.second;
         SASSERT(idx < m_bits[v1].size());
@@ -433,7 +465,7 @@ namespace bv {
         lbool   val = s().value(bit1);
         TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_expr_id() << "[" << idx << "] = " << val << "\n";);
         if (val == l_undef)
-            return;
+            return false;
 
         if (val == l_false)
             bit1.neg();
@@ -447,7 +479,7 @@ namespace bv {
             if (val == l_false)
                 bit2.neg();
             ++num_bits;
-            if (num_bits > 4 && num_assigned == 0)
+            if (num_bits > 3 && num_assigned == 0)
                 break;
             if (s().value(bit2) == l_true) 
                 continue;
@@ -455,7 +487,7 @@ namespace bv {
             if (!assign_bit(bit2, v1, v2, idx, bit1, false))
                 break;
         }
-        // std::cout << num_bits << " " << num_assigned << "\n"; 
+        return num_assigned > 0;
     }
 
     sat::check_result solver::check() {
@@ -590,10 +622,10 @@ namespace bv {
         st.update("bv conflicts", m_stats.m_num_conflicts);
         st.update("bv diseqs", m_stats.m_num_diseq_static);
         st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
-        st.update("bv eq2bit", m_stats.m_num_bit2core);
-        st.update("bv ne2bit", m_stats.m_num_nbit2core);
-        st.update("bv bit2eq", m_stats.m_num_th2core_eq);
-        st.update("bv bit2ne", m_stats.m_num_th2core_diseq);
+        st.update("bv eq2bit", m_stats.m_num_eq2bit);
+        st.update("bv ne2bit", m_stats.m_num_ne2bit);
+        st.update("bv bit2eq", m_stats.m_num_bit2eq);
+        st.update("bv bit2ne", m_stats.m_num_bit2ne);
         st.update("bv ackerman", m_stats.m_ackerman);
     }
 
@@ -625,6 +657,12 @@ namespace bv {
                 m_bool_var2atom.setx(i, new_a, nullptr);
                 for (auto vp : a->to_bit())
                     new_a->m_occs = new (result->get_region()) var_pos_occ(vp.first, vp.second, new_a->m_occs);
+                for (auto const& occ : a->to_bit().eqs()) {
+                    expr* e = occ.m_node->get_expr();
+                    expr_ref e2(tr(e), tr.to());
+                    euf::enode* n = ctx.get_enode(e2);
+                    new_a->m_eqs = new (result->get_region()) eq_occurs(occ.m_bv1, occ.m_bv2, occ.m_idx, occ.m_v1, occ.m_v2, occ.m_literal, n, new_a->m_eqs);
+                }
             }
             else {
                 def_atom* new_a = new (result->get_region()) def_atom(a->to_def().m_var, a->to_def().m_def);
@@ -669,6 +707,7 @@ namespace bv {
     }
 
     void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
+
         TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";);
         if (!merge_zero_one_bits(r1, r2)) {
             TRACE("bv", tout << "conflict detected\n";);
@@ -676,10 +715,16 @@ namespace bv {
         }
         SASSERT(m_bits[v1].size() == m_bits[v2].size());
         unsigned sz = m_bits[v1].size();
+        if (sz == 1)
+            return;
         for (unsigned idx = 0; !s().inconsistent() && idx < sz; idx++) {
             literal bit1 = m_bits[v1][idx];
             literal bit2 = m_bits[v2][idx];
             CTRACE("bv", bit1 == ~bit2, tout << pp(v1) << pp(v2) << "idx: " << idx << "\n";);
+            if (bit1 == ~bit2) {
+                mk_new_diseq_axiom(v1, v2, idx);
+                return;
+            }
             SASSERT(bit1 != ~bit2);
             lbool val1 = s().value(bit1);
             lbool val2 = s().value(bit2);
@@ -729,7 +774,7 @@ namespace bv {
 
     bool solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
 
-        m_stats.m_num_bit2core++;
+        m_stats.m_num_eq2bit++;
         SASSERT(ctx.s().value(antecedent) == l_true);
         SASSERT(m_bits[v2][idx].var() == consequent.var());
         SASSERT(consequent.var() != antecedent.var());
@@ -740,14 +785,6 @@ namespace bv {
             return false;
         }
         else {
-            if (false && get_config().m_bv_eq_axioms) {
-                expr_ref eq = mk_var_eq(v1, v2);
-                flet<bool> _is_redundant(m_is_redundant, true);
-                literal eq_lit = ctx.internalize(eq, false, false, m_is_redundant);
-                add_clause(~antecedent, ~eq_lit, consequent);
-                add_clause(antecedent, ~eq_lit, ~consequent);
-            }
-
             if (m_wpos[v2] == idx)
                 find_wpos(v2);
             bool_var cv = consequent.var();
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index 8b4153783..0b8f51683 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -44,7 +44,7 @@ namespace bv {
 
         struct stats {
             unsigned   m_num_diseq_static, m_num_diseq_dynamic,  m_num_conflicts;
-            unsigned   m_num_bit2core, m_num_th2core_eq, m_num_th2core_diseq, m_num_nbit2core;
+            unsigned   m_num_bit2eq, m_num_bit2ne, m_num_eq2bit, m_num_ne2bit;
             unsigned   m_ackerman;
             void reset() { memset(this, 0, sizeof(stats)); }
             stats() { reset(); }
@@ -106,14 +106,53 @@ namespace bv {
 
         typedef svector<zero_one_bit> zero_one_bits;
 
+        struct eq_occurs {
+            sat::bool_var m_bv1;
+            sat::bool_var m_bv2;
+            unsigned    m_idx;
+            theory_var  m_v1;
+            theory_var  m_v2;
+            sat::literal m_literal;
+            euf::enode* m_node;
+            eq_occurs* m_next;
+            eq_occurs* m_prev;
+            eq_occurs(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, sat::literal lit, euf::enode* n, eq_occurs* next = nullptr) :
+                m_bv1(b1), m_bv2(b2), m_idx(idx), m_v1(v1), m_v2(v2), m_literal(lit), m_node(n), m_next(next), m_prev(nullptr) {}
+        };
+
+        class eq_occurs_it {
+            eq_occurs* m_first;
+        public:
+            eq_occurs_it(eq_occurs* c) : m_first(c) {}
+            eq_occurs operator*() { return *m_first; }
+            eq_occurs_it& operator++() { m_first = m_first->m_next; return *this; }
+            eq_occurs_it operator++(int) { eq_occurs_it tmp = *this; ++* this; return tmp; }
+            bool operator==(eq_occurs_it const& other) const { return m_first == other.m_first; }
+            bool operator!=(eq_occurs_it const& other) const { return !(*this == other); }
+        };
+
+        class eqs_iterator {
+            eq_occurs* o;
+        public:
+            eqs_iterator(eq_occurs* o) :o(o) {}
+            eq_occurs_it begin() const { return eq_occurs_it(o); }
+            eq_occurs_it end() const { return eq_occurs_it(nullptr); }
+        };
+
         struct bit_atom;
         struct def_atom;
+        struct eq_atom;
         class atom {
         public:
+
+            atom()  {}
             virtual ~atom() {}
-            virtual bool is_bit() const = 0;
+            virtual bool is_bit() const { return false; }
+            virtual bool is_eq() const { return false; }
             bit_atom& to_bit();
             def_atom& to_def();
+            eq_atom& to_eq();
+
         };
 
         struct var_pos_occ {
@@ -133,47 +172,24 @@ namespace bv {
             bool operator!=(var_pos_it const& other) const { return !(*this == other); }
         };
 
-        struct eq_occurs {
-            unsigned    m_idx;
-            theory_var  m_v1;
-            theory_var  m_v2;
-            sat::literal m_literal;
-            euf::enode* m_node;
-            eq_occurs*  m_next;
-            eq_occurs(unsigned idx, theory_var v1, theory_var v2, sat::literal lit, euf::enode* n, eq_occurs* next = nullptr):
-                m_idx(idx), m_v1(v1), m_v2(v2), m_literal(lit), m_node(n), m_next(next) {}
-        };
-
-        class eq_occurs_it {
-            eq_occurs* m_first;
-        public:
-            eq_occurs_it(eq_occurs* c) : m_first(c) {}
-            eq_occurs operator*() { return *m_first; }
-            eq_occurs_it& operator++() { m_first = m_first->m_next; return *this; }
-            eq_occurs_it operator++(int) { eq_occurs_it tmp = *this; ++* this; return tmp; }
-            bool operator==(eq_occurs_it const& other) const { return m_first == other.m_first; }
-            bool operator!=(eq_occurs_it const& other) const { return !(*this == other); }
-        };
-
         struct bit_atom : public atom {
+            eq_occurs*    m_eqs;
             var_pos_occ * m_occs;
-            eq_occurs   * m_eqs;
-            bit_atom():m_occs(nullptr), m_eqs(nullptr) {}
+            bit_atom() :m_eqs(nullptr), m_occs(nullptr) {}
             ~bit_atom() override {}
             bool is_bit() const override { return true; }
             var_pos_it begin() const { return var_pos_it(m_occs); }
             var_pos_it end() const { return var_pos_it(nullptr); }
             bool is_fresh() const { return !m_occs && !m_eqs; }
-            
-            class eqs_iterator {
-                bit_atom const& a;
-            public:
-                eqs_iterator(bit_atom const& a):a(a) {}
-                eq_occurs_it begin() const { return eq_occurs_it(a.m_eqs); }
-                eq_occurs_it end() const { return eq_occurs_it(nullptr); }
-            };
+            eqs_iterator eqs() const { return eqs_iterator(m_eqs); }           
+        };
 
-            eqs_iterator eqs() const { return eqs_iterator(*this); }
+        struct eq_atom : public atom {
+            eq_atom(){}
+            ~eq_atom() override { m_eqs.clear();  }
+            bool is_bit() const override { return false; }
+            bool is_eq() const override { return true; }
+            svector<std::pair<bit_atom*,eq_occurs*>> m_eqs;
         };
 
         struct def_atom : public atom {
@@ -181,7 +197,6 @@ namespace bv {
             literal    m_def;
             def_atom(literal v, literal d):m_var(v), m_def(d) {}
             ~def_atom() override {}
-            bool is_bit() const override { return false; }
         };
 
         struct propagation_item {
@@ -195,6 +210,7 @@ namespace bv {
         class bit_trail;
         class add_var_pos_trail;
         class add_eq_occurs_trail;
+        class del_eq_occurs_trail;
         class mk_atom_trail;
         class bit_occs_trail;
         typedef ptr_vector<atom> bool_var2atom;
@@ -242,8 +258,10 @@ namespace bv {
         sat::status status() const { return sat::status::th(m_is_redundant, get_id());  }
         void register_true_false_bit(theory_var v, unsigned i);
         void add_bit(theory_var v, sat::literal lit);
-        bit_atom* mk_bit_atom(sat::bool_var bv);
-        void eq_internalized(sat::bool_var b, unsigned idx, theory_var v1, theory_var v2, euf::enode* n);
+        bit_atom* mk_bit_atom(sat::bool_var b);
+        eq_atom* mk_eq_atom(sat::bool_var b);
+        void eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, sat::literal eq, euf::enode* n);
+        void del_eq_occurs(bit_atom* a, eq_occurs* occ);
 
         void set_bit_eh(theory_var v, literal l, unsigned idx);
         void init_bits(expr* e, expr_ref_vector const & bits);
@@ -280,8 +298,8 @@ namespace bv {
         svector<theory_var>   m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
         bool merge_zero_one_bits(theory_var r1, theory_var r2);
         bool assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
-        void propagate_bits(var_pos entry);
-        void propagate_eq_occurs(eq_occurs const& occ);
+        bool propagate_bits(var_pos entry);
+        bool propagate_eq_occurs(eq_occurs const& occ);
         numeral const& power2(unsigned i) const;
 
         // invariants
@@ -348,7 +366,7 @@ namespace bv {
         void unmerge_eh(theory_var v1, theory_var v2);
         trail_stack<euf::solver>& get_trail_stack();
 
-        // disagnostics
+        // diagnostics
         std::ostream& display(std::ostream& out, theory_var v) const;        
         typedef std::pair<solver const*, theory_var> pp_var;
         pp_var pp(theory_var v) const { return pp_var(this, v); }
diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp
index d65bc7510..71ec213af 100644
--- a/src/sat/smt/euf_ackerman.cpp
+++ b/src/sat/smt/euf_ackerman.cpp
@@ -74,8 +74,13 @@ namespace euf {
             new_tmp();        
         }
         other->m_count++;
-        if (other->m_count > m_high_watermark) 
-            s.s().set_should_simplify();
+        if (other->m_count > m_high_watermark) {
+            if (other->is_cc)
+                add_cc(other->a, other->b);
+            else
+                add_eq(other->a, other->b, other->c);
+            other->m_count = 0;
+        }       
         inference::push_to_front(m_queue, other);
     }
 
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index b91e5c1a3..144494c33 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -31,6 +31,14 @@ namespace euf {
     }
 
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        euf::enode* n = m_egraph.find(e);
+        if (n) {
+            if (m.is_bool(e)) {
+                VERIFY(!s().was_eliminated(n->bool_var()));
+                return literal(n->bool_var(), sign);
+            }
+            return sat::null_literal;
+        }
         if (si.is_bool_op(e))
             return attach_lit(si.internalize(e, redundant), e);
         if (auto* ext = expr2solver(e))
@@ -117,9 +125,13 @@ namespace euf {
             s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
             lit = lit2;
         }
+
         m_var2expr.reserve(v + 1, nullptr);
-        if (m_var2expr[v])
+        if (m_var2expr[v]) {
+            SASSERT(m_egraph.find(e));
+            SASSERT(m_egraph.find(e)->bool_var() == v);
             return lit;
+        }
         m_var2expr[v] = e;
         m_var_trail.push_back(v);
         enode* n = m_egraph.find(e);
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 60840591a..d63532bbf 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -227,7 +227,7 @@ namespace euf {
         size_t* c = to_ptr(l);
         SASSERT(is_literal(c));
         SASSERT(l == get_literal(c));
-        if (m.is_eq(e) && n->num_args() == 2 && !sign) {
+        if (!sign && n->is_equality()) {
             SASSERT(!m.is_iff(e));
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
@@ -237,9 +237,8 @@ namespace euf {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
         }
-        else if (m.is_eq(e) && n->num_args() == 2 && sign) {
-            m_egraph.new_diseq(n);
-        }
+        else if (sign && n->is_equality())
+            m_egraph.new_diseq(n);        
     }
 
 
@@ -462,20 +461,23 @@ namespace euf {
     }
 
     bool solver::set_root(literal l, literal r) {
+        expr* e = bool_var2expr(l.var());
+        if (!e)
+            return true;
         bool ok = true;
         for (auto* s : m_solvers)
             if (!s->set_root(l, r))
                 ok = false;
-        expr* e = bool_var2expr(l.var());
-        if (e) {
-            if (m.is_eq(e) && !m.is_iff(e))
-                ok = false;
-            euf::enode* n = get_enode(e);
-            if (n && n->merge_enabled())
-                ok = false;
-        }
+        if (m.is_eq(e) && !m.is_iff(e))
+            ok = false;
+        euf::enode* n = get_enode(e);
+        if (n && n->merge_enabled())
+            ok = false;
+        
+        (void)ok;
         TRACE("euf", tout << ok << " " << l << " -> " << r << "\n";);
-        return ok;
+        // roots cannot be eliminated as long as the egraph contains the expressions.
+        return false;
     }
 
     void solver::flush_roots() {
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index eed5d7cb0..4e408fdab 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -157,6 +157,7 @@ namespace euf {
         enode* var2enode(theory_var v) const { return m_var2enode[v]; }
         expr* var2expr(theory_var v) const { return var2enode(v)->get_expr(); }
         expr* bool_var2expr(sat::bool_var v) const;
+        enode* bool_var2enode(sat::bool_var v) const { expr* e = bool_var2expr(v); return e ? expr2enode(e) : nullptr; }
         expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
         theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
         theory_var get_th_var(expr* e) const;
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 91daf23c4..b561ff287 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -219,6 +219,7 @@ namespace smt {
         {
             std::function<expr*(void)> fn = [&]() { return m.mk_or(bound, m.mk_not(bound)); };
             scoped_trace_stream _sts(*this, fn);
+            IF_VERBOSE(10, verbose_stream() << "branch " << bound << "\n");
             TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";);
             ctx.internalize(bound, true);
             ctx.mark_as_relevant(bound.get());
@@ -296,7 +297,7 @@ namespace smt {
                     continue;
                 }
                 if (!is_int(x)) {
-                    TRACE("theory_arith_int", display_row(tout << "!int:  ", r, true); );
+                    TRACE("arith_int", display_row(tout << "!int:  ", r, true); );
                     is_tight = false;
                     continue;
                 }
@@ -324,7 +325,7 @@ namespace smt {
                     row[i] *= denom.to_rational();
                 }
             }
-            TRACE("theory_arith_int",
+            TRACE("arith_int",
                   tout << "extracted row:\n";
                   for (unsigned i = 0; i < max_row; ++i) {
                       tout << row[i] << " ";
@@ -365,7 +366,7 @@ namespace smt {
             }
         }            
         if (pol.empty()) {
-            TRACE("theory_arith_int", tout << "The witness is trivial\n";);
+            TRACE("arith_int", tout << "The witness is trivial\n";);
             return false;
         }
         expr_ref p1(get_manager()), p2(get_manager());
@@ -419,6 +420,7 @@ namespace smt {
                     scoped_trace_stream _sts(*this, fn);
                     ctx.internalize(bound, true);
                 }
+                IF_VERBOSE(10, verbose_stream() << "free " << bound << "\n");
                 ctx.mark_as_relevant(bound.get());
                 result = true;
             }
@@ -672,6 +674,7 @@ namespace smt {
             ctx.internalize(bound, true);
         }
         l = ctx.get_literal(bound);
+        IF_VERBOSE(10, verbose_stream() << "cut " << bound << "\n");
         ctx.mark_as_relevant(l);
         dump_lemmas(l, ante);
         auto js = ctx.mk_justification(
diff --git a/src/util/heap.h b/src/util/heap.h
index 4651012aa..7a348aa4d 100644
--- a/src/util/heap.h
+++ b/src/util/heap.h
@@ -158,6 +158,10 @@ public:
         return m_value2indices.size();
     }
 
+    unsigned size() const {
+        return m_value2indices.size();
+    }
+
     void reserve(int s) {
         CASSERT("heap", check_invariant());
         if (s > static_cast<int>(m_value2indices.size()))