diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 80e50c61561..c2ff7939d09 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -573,30 +573,30 @@ namespace euf {
 
     std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
         out << n->get_expr_id() << " := ";
-        if (!n->is_root()) 
-            out << "[" << n->get_root()->get_expr_id() << "] ";
         expr* f = n->get_expr();
         if (is_app(f))
-            out << mk_bounded_pp(f, m, 1);
+            out << mk_bounded_pp(f, m, 1) << " ";
         else if (is_quantifier(f))
-            out << "q:" << f->get_id();
+            out << "q:" << f->get_id() << " ";
         else
-            out << "v:" << f->get_id();
-        out << "\n";
+            out << "v:" << f->get_id() << " ";
+        if (!n->is_root()) 
+            out << "[r " << n->get_root()->get_expr_id() << "] ";
         if (!n->m_parents.empty()) {
-            out << "    parents ";
+            out << "[p";
             for (enode* p : enode_parents(n))
-                out << p->get_expr_id() << " ";
-            out << "\n";
+                out << " " << p->get_expr_id();
+            out << "] ";
         }
         if (n->has_th_vars()) {
-            out << "    theories ";
+            out << "[t";
             for (auto v : enode_th_vars(n))
-                out << v.get_id() << ":" << v.get_var() << " ";
-            out << "\n";
+                out << " " << v.get_id() << ":" << v.get_var();
+            out << "] ";
         }
         if (n->m_target && m_display_justification)
-            n->m_justification.display(out << "    = " << n->m_target->get_expr_id() << " j: ", m_display_justification) << "\n";
+            n->m_justification.display(out << "[j " << n->m_target->get_expr_id() << " ", m_display_justification) << "] ";
+        out << "\n";
         return out;
     }
 
diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp
index 2ca17e344da..510593bbf0a 100644
--- a/src/sat/sat_probing.cpp
+++ b/src/sat/sat_probing.cpp
@@ -237,6 +237,7 @@ namespace sat {
         if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit)
             m_cached_bins.finalize();
 
+        flet<bool> _probing(m_active, true);
         report rpt(*this);
         bool r    = true;
         m_counter = 0;
diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h
index 986bad6a8d6..dd75d21bfbc 100644
--- a/src/sat/sat_probing.h
+++ b/src/sat/sat_probing.h
@@ -31,7 +31,7 @@ namespace sat {
         unsigned        m_stopped_at;  // where did it stop
         literal_set     m_assigned;    // literals assigned in the first branch
         literal_vector  m_to_assert;
-
+        bool            m_active { false };
         // counters
         int             m_counter;       // track cost
 
@@ -78,6 +78,7 @@ namespace sat {
 
         void collect_statistics(statistics & st) const;
         void reset_statistics();
+        bool active() const { return m_active; }
 
         // return the literals implied by l.
         // return 0, if the cache is not available
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index daa4b3e5aa7..3219d7d605f 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1934,12 +1934,24 @@ namespace sat {
         }
         log_stats();
         m_simplifications++;
-        IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";);
 
         TRACE("sat", tout << "simplify\n";);
 
         pop(scope_lvl());
-
+        struct report {
+            solver&   s;
+            stopwatch m_watch;
+            report(solver& s):s(s) { 
+                m_watch.start(); 
+                s.log_stats();
+                IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << s.m_simplifications << ")\n";);
+            }
+            ~report() { 
+                m_watch.stop(); 
+                s.log_stats();
+            }
+        };
+        report _rprt(*this);
         SASSERT(at_base_lvl());
 
         m_cleaner(m_config.m_force_cleanup);
@@ -3943,9 +3955,8 @@ namespace sat {
             break;
         }
         case justification::EXT_JUSTIFICATION:
-            if (m_ext) {
-                m_ext->display_justification(out << " ", js.get_ext_justification_idx());
-            }
+            if (m_ext) 
+                m_ext->display_justification(out, js.get_ext_justification_idx());            
             break;
         default:
             break;
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 00ade9465f6..abd4a66d292 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -662,6 +662,7 @@ namespace sat {
     public:
         void set_should_simplify() { m_next_simplify = m_conflicts_since_init; }
         bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit;  }
+        bool is_probing() const { return m_probing.active(); }
 
     public:
         void user_push() override;
diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp
index 1d7ebfe13ee..beee6a558fc 100644
--- a/src/sat/smt/bv_ackerman.cpp
+++ b/src/sat/smt/bv_ackerman.cpp
@@ -110,7 +110,7 @@ namespace bv {
         }
         
         if (glue < max_glue) 
-            v.m_glue = 2*glue <= sz ? 0 : glue;
+            v.m_glue = (sz > 6 && 2*glue <= sz) ? 0 : glue;
     }
 
     void ackerman::remove(vv* p) {
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 6a46dbe45d5..376d4c69e94 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -42,6 +42,16 @@ namespace bv {
         }
     };
 
+    class solver::add_eq_occurs_trail : public trail<euf::solver> {
+        solver::bit_atom* m_atom;
+    public:
+        add_eq_occurs_trail(solver::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;
+        }
+    };    
+
     class solver::mk_atom_trail : public trail<euf::solver> {
         solver& th;
         sat::bool_var m_var;
@@ -242,10 +252,15 @@ namespace bv {
     }
 
     solver::bit_atom* solver::mk_bit_atom(sat::bool_var bv) {
-        bit_atom* b = new (get_region()) bit_atom();
-        insert_bv2a(bv, b);
-        ctx.push(mk_atom_trail(bv, *this));
-        return b;
+        atom* a = get_bv2a(bv);
+        if (a) 
+            return a->is_bit() ? &a->to_bit() : nullptr;
+        else {
+            bit_atom* b = new (get_region()) bit_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) {
@@ -253,20 +268,14 @@ namespace bv {
         if (s().value(l) != l_undef && s().lvl(l) == 0) 
             register_true_false_bit(v, idx);
         else {
-            atom* a = get_bv2a(l.var());
-            if (a && !a->is_bit()) 
-                ;
-            else if (a) {
-                bit_atom* b = &a->to_bit();
-                find_new_diseq_axioms(*b, v, idx);
-                ctx.push(add_var_pos_trail(b));
+            bit_atom* b = mk_bit_atom(l.var());
+            if (b) {
+                if (b->m_occs)
+                    find_new_diseq_axioms(*b, v, idx);
+                if (!b->is_fresh()) 
+                    ctx.push(add_var_pos_trail(b));                
                 b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
             }
-            else {
-                bit_atom* b = mk_bit_atom(l.var());
-                SASSERT(!b->m_occs);
-                b->m_occs = new (get_region()) var_pos_occ(v, idx);
-            }
         }
     }
 
@@ -570,12 +579,34 @@ namespace bv {
         }
     }
 
+    void solver::eq_internalized(euf::enode* n) {
+        SASSERT(m.is_eq(n->get_expr()));
+        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);
+        unsigned sz = m_bits[v1].size();
+        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);
+        }
+    }
+
+    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);
+        if (a) {
+            if (!a->is_fresh()) 
+                ctx.push(add_eq_occurs_trail(a));
+            a->m_eqs = new (get_region()) eq_occurs(idx, v1, v2, n, a->m_eqs);
+        }
+    }
+
     void solver::assert_ackerman(theory_var v1, theory_var v2) {
         if (v1 == v2)
             return;
         if (v1 > v2)
             std::swap(v1, v2);
-        flet<bool> _red(m_is_redundant, true);        
+        flet<bool> _red(m_is_redundant, true);
         ++m_stats.m_ackerman;
         expr* o1 = var2expr(v1);
         expr* o2 = var2expr(v2);
@@ -584,6 +615,7 @@ namespace bv {
         unsigned sz = m_bits[v1].size();
         TRACE("bv", tout << "ackerman-eq: " << s().scope_lvl() << " " << oe << "\n";);
         literal_vector eqs;
+        eqs.push_back(oeq);
         for (unsigned i = 0; i < sz; ++i) {
             literal l1 = m_bits[v1][i];
             literal l2 = m_bits[v2][i];
@@ -592,14 +624,10 @@ namespace bv {
             e2 = bv.mk_bit2bool(o2, i);
             expr_ref e = mk_eq(e1, e2);
             literal eq = ctx.internalize(e, false, false, m_is_redundant);
-            add_clause(l1, ~l2, ~eq);
-            add_clause(~l1, l2, ~eq);
-            add_clause(l1, l2, eq);
-            add_clause(~l1, ~l2, eq);
             add_clause(eq, ~oeq);
             eqs.push_back(~eq);
         }
-        eqs.push_back(oeq);
+        TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);
         s().add_clause(eqs.size(), eqs.c_ptr(), sat::status::th(m_is_redundant, get_id()));
     }
 }
diff --git a/src/sat/smt/bv_invariant.cpp b/src/sat/smt/bv_invariant.cpp
index 73db67894be..82fde885e1e 100644
--- a/src/sat/smt/bv_invariant.cpp
+++ b/src/sat/smt/bv_invariant.cpp
@@ -16,6 +16,7 @@ Module Name:
 --*/
 
 #include "sat/smt/bv_solver.h"
+#include "sat/smt/euf_solver.h"
 
 namespace bv {
 
@@ -32,6 +33,27 @@ namespace bv {
         }
     }
 
+    void solver::check_missing_propagation() const {
+        for (euf::enode* n : ctx.get_egraph().nodes()) {
+            expr* e = n->get_expr(), *a = nullptr, *b = nullptr;
+            if (m.is_eq(e, a, b) && bv.is_bv(a) && s().value(expr2literal(e)) == l_undef) {
+                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);
+                unsigned sz = m_bits[v1].size();
+                for (unsigned i = 0; i < sz; ++i) {
+                    lbool val1 = s().value(m_bits[v1][i]);
+                    lbool val2 = s().value(m_bits[v2][i]);
+                    if (val1 != l_undef && val2 != l_undef && val1 != val2) {
+                        IF_VERBOSE(0, verbose_stream() << "missing " << mk_bounded_pp(e, m) << "\n");
+                        break;
+                    }
+                }
+            }
+        }
+    }
+
     /**
         \brief Check whether m_zero_one_bits is an accurate summary of the bits in the
         equivalence class rooted by v.
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index a356f5890e6..e022fcb918b 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -69,7 +69,7 @@ namespace bv {
             m_fixed_var_table.find(key, v2) &&
             v2 < static_cast<int>(get_num_vars()) &&
             is_bv(v2) &&
-            get_bv_size(v2) == sz &&
+            m_bits[v2].size() == sz &&
             get_fixed_value(v2, val2) && val1 == val2;
 
         if (!is_current)
@@ -79,7 +79,7 @@ namespace bv {
             TRACE("bv", tout << "detected equality: v" << v1 << " = v" << v2 << "\n" << pp(v1) << pp(v2););
             m_stats.m_num_th2core_eq++;
             add_fixed_eq(v1, v2);
-            ctx.propagate(var2enode(v1), var2enode(v2), mk_bit2bv_justification(v1, v2));
+            ctx.propagate(var2enode(v1), var2enode(v2), mk_bit2eq_justification(v1, v2));
         }
     }
 
@@ -137,7 +137,7 @@ namespace bv {
         for (auto vp : a) {
             theory_var v2 = vp.first;
             unsigned   idx2 = vp.second;
-            if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v))
+            if (idx == idx2 && m_bits[v2].size() == m_bits[v].size() && m_bits[v2][idx2] == l )
                 mk_new_diseq_axiom(v, v2, idx);
         }
     }
@@ -149,8 +149,6 @@ namespace bv {
         if (!get_config().m_bv_eq_axioms)
             return;
 
-        // TBD: disabled until new literal creation is supported
-        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++;
@@ -195,7 +193,7 @@ namespace bv {
 
     void solver::new_eq_eh(euf::th_eq const& eq) {
         force_push();
-        TRACE("bv", tout << "new eq " << eq.v1() << " == " << eq.v2() << "\n";);
+        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()))
             m_find.merge(eq.v1(), eq.v2());
     }
@@ -204,11 +202,13 @@ namespace bv {
         theory_var v1 = ne.v1(), v2 = ne.v2();
         if (!is_bv(v1))
             return;
-        if (!get_config().m_bv_eq_axioms)
+        if (s().is_probing())
             return;
-
-        TRACE("bv", tout << "diff: " << v1 << " != " << v2 << "\n";);
+        
+        TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
         unsigned sz = m_bits[v1].size();
+        unsigned num_undef = 0;
+        int undef_idx = 0;
         for (unsigned i = 0; i < sz; ++i) {
             sat::literal a = m_bits[v1][i];
             sat::literal b = m_bits[v2][i];
@@ -218,12 +218,41 @@ namespace bv {
             auto vb = s().value(b);
             if (va != l_undef && vb != l_undef && va != vb)
                 return;
+            if (va == l_undef) {
+                ++num_undef;
+                undef_idx = i + 1;
+            }
+            if (vb == l_undef) {
+                ++num_undef;
+                undef_idx = -static_cast<int>(i + 1);
+            }
+            if (num_undef > 1 && get_config().m_bv_eq_axioms)
+                return;
+        }
+        if (num_undef == 0)
+            return;
+        else if (num_undef == 1) {
+            if (undef_idx < 0) {
+                undef_idx = -undef_idx;
+                std::swap(v1, v2);
+            }
+            undef_idx--;
+            sat::literal consequent = m_bits[v1][undef_idx];
+            sat::literal b = m_bits[v2][undef_idx];
+            sat::literal antecedent = ~expr2literal(ne.eq());
+            SASSERT(s().value(antecedent) == l_true);
+            SASSERT(s().value(consequent) == l_undef);
+            SASSERT(s().value(b) != l_undef);
+            if (s().value(b) == l_true)
+                consequent.neg();
+            ++m_stats.m_num_nbit2core;
+            s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent));
         }
-        if (s().at_search_lvl()) {
+        else if (s().at_search_lvl()) {
             force_push();
             assert_ackerman(v1, v2);
         }
-        else
+        else         
             m_ackerman.used_diseq_eh(v1, v2);        
     }
 
@@ -236,12 +265,41 @@ namespace bv {
         auto& c = bv_justification::from_index(idx);
         TRACE("bv", display_constraint(tout, idx););
         switch (c.m_kind) {
-        case bv_justification::kind_t::bv2bit:
+        case bv_justification::kind_t::eq2bit:
             SASSERT(s().value(c.m_antecedent) == l_true);
             r.push_back(c.m_antecedent);
             ctx.add_antecedent(var2enode(c.m_v1), var2enode(c.m_v2));
             break;
-        case bv_justification::kind_t::bit2bv:
+        case bv_justification::kind_t::ne2bit: {
+            r.push_back(c.m_antecedent);
+            SASSERT(s().value(c.m_antecedent) == l_true);
+            SASSERT(c.m_consequent == l);
+            unsigned idx = c.m_idx;
+            for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) {
+                sat::literal a = m_bits[c.m_v1][i];
+                sat::literal b = m_bits[c.m_v2][i];
+                SASSERT(a == b || s().value(a) != l_undef);
+                SASSERT(i == idx || s().value(a) == s().value(b));
+                if (a == b)
+                    continue;
+                if (i == idx) {
+                    if (s().value(b) == l_false)
+                        b.neg();
+                    r.push_back(b);
+                    
+                    continue;
+                }
+                if (s().value(a) == l_false) {
+                    a.neg();
+                    b.neg();
+                }
+                r.push_back(a);
+                r.push_back(b);
+            }
+            
+            break;
+        }
+        case bv_justification::kind_t::bit2eq:
             SASSERT(m_bits[c.m_v1].size() == m_bits[c.m_v2].size());
             for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) {
                 sat::literal a = m_bits[c.m_v1][i];
@@ -258,6 +316,25 @@ namespace bv {
                 r.push_back(b);
             }
             break;
+        case bv_justification::kind_t::bit2ne: {
+            SASSERT(c.m_consequent.sign());
+            sat::bool_var v = c.m_consequent.var();
+            expr* eq = bool_var2expr(v);
+            SASSERT(m.is_eq(eq));
+            euf::enode* n = expr2enode(eq);
+            theory_var v1 = n->get_arg(0)->get_th_var(get_id());
+            theory_var v2 = n->get_arg(1)->get_th_var(get_id());
+            sat::literal a = m_bits[v1][c.m_idx];
+            sat::literal b = m_bits[v2][c.m_idx];
+            lbool val_a = s().value(a);
+            lbool val_b = s().value(b);
+            SASSERT(val_a != l_undef && val_b != l_undef && val_a != val_b);
+            if (val_a == l_false) a.neg();
+            if (val_b == l_false) b.neg();
+            r.push_back(a);
+            r.push_back(b);
+            break;
+        }
         }
         if (!probing && ctx.use_drat())
             log_drat(c);
@@ -274,42 +351,41 @@ namespace bv {
         ctx.get_drat().def_add_arg(e2->get_id());
         ctx.get_drat().def_end();
         ctx.get_drat().bool_def(leq.var(), eq->get_id());
+
         sat::literal_vector lits;
-        auto add_bit = [&](sat::literal lit) {
-            if (s().value(lit) == l_true)
-                lit.neg();
-            lits.push_back(lit);
-        };
         switch (c.m_kind) {
-        case bv_justification::kind_t::bv2bit:
+        case bv_justification::kind_t::eq2bit:
             lits.push_back(~leq);
             lits.push_back(~c.m_antecedent);
             lits.push_back(c.m_consequent);
             break;
-        case bv_justification::kind_t::bit2bv:
+        case bv_justification::kind_t::ne2bit:
+            get_antecedents(c.m_consequent, c.to_index(), lits, true);
+            lits.push_back(c.m_consequent);
+            break;
+        case bv_justification::kind_t::bit2eq:      
+            get_antecedents(leq, c.to_index(), lits, true);
+            for (auto& lit : lits)
+                lit.neg();
             lits.push_back(leq);
-            for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) {
-                sat::literal a = m_bits[c.m_v1][i];
-                sat::literal b = m_bits[c.m_v2][i];
-                if (a != b) {
-                    add_bit(a);
-                    add_bit(b);
-                }
-            }
+            break;
+        case bv_justification::kind_t::bit2ne: 
+            get_antecedents(c.m_consequent, c.to_index(), lits, true);
+            for (auto& lit : lits)
+                lit.neg();
+            lits.push_back(c.m_consequent);            
             break;
         }
         ctx.get_drat().add(lits, status());
-        ctx.get_drat().log_gc_var(leq.var());
+        ctx.get_drat().log_gc_var(leq.var()); // TBD, a proper way would be to delete the lemma after use.
     }
 
     void solver::asserted(literal l) {
-
         atom* a = get_bv2a(l.var());
         TRACE("bv", tout << "asserted: " << l << "\n";);
         if (a && a->is_bit()) {
             force_push();
-            for (auto vp : a->to_bit())
-                m_prop_queue.push_back(vp);
+            m_prop_queue.push_back(propagation_item(&a->to_bit()));
         }
     }
 
@@ -318,11 +394,34 @@ namespace bv {
             return false;
         force_push();
         ctx.push(value_trail<euf::solver, unsigned>(m_prop_queue_head));
-        for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head)
-            propagate_bits(m_prop_queue[m_prop_queue_head]);
+        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);
+            }
+            else 
+                propagate_bits(p.m_vp);            
+        }
+        // check_missing_propagation();
         return true;
     }
 
+    void solver::propagate_eq_occurs(eq_occurs const& occ) {
+        auto lit = expr2literal(occ.m_node->get_expr());
+        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]);
+        SASSERT(val1 != l_undef);
+        if (val1 != val2 && val2 != l_undef) {
+            ++m_stats.m_num_th2core_diseq;
+            s().assign(~lit, mk_bit2ne_justification(occ.m_idx, ~lit));
+        }
+    }
+
     void solver::propagate_bits(var_pos entry) {
         theory_var v1 = entry.first;
         unsigned idx = entry.second;
@@ -453,11 +552,25 @@ namespace bv {
 
     std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
         auto& c = bv_justification::from_index(idx);
+        theory_var v1 = c.m_v1;
+        theory_var v2 = c.m_v2;
+        unsigned cidx = c.m_idx;
         switch (c.m_kind) {
-        case bv_justification::kind_t::bv2bit:
-            return out << c.m_consequent << " <= " << c.m_antecedent << " v" << c.m_v1 << " == v" << c.m_v2 << "\n";
-        case bv_justification::kind_t::bit2bv:
-            return out << m_bits[c.m_v1] << " == " << m_bits[c.m_v2] << " => v" << c.m_v1 << " == v" << c.m_v2 << "\n";
+        case bv_justification::kind_t::eq2bit:
+            return out << "bv <- " << c.m_antecedent << " v" << v1 << " == v" << v2;
+        case bv_justification::kind_t::bit2eq:
+            return out << "bv " << m_bits[v1] << " == " << m_bits[v2] << " -> v" << v1 << " == v" << v2;
+        case bv_justification::kind_t::bit2ne: {
+            expr* e = bool_var2expr(c.m_consequent.var());
+            SASSERT(m.is_eq(e));
+            euf::enode* n = expr2enode(e);
+            v1 = n->get_arg(0)->get_th_var(get_id());
+            v2 = n->get_arg(1)->get_th_var(get_id());            
+            return out << "bv <- v" << v1 << "[" << cidx << "] != v" << v2 << "[" << cidx << "] " << m_bits[v1][cidx] << " != " << m_bits[v2][cidx];
+        }
+        case bv_justification::kind_t::ne2bit: 
+            return out << "bv <- " << m_bits[v1] << " != " << m_bits[v2] << " @" << cidx;
+            break;                                                     
         default:
             UNREACHABLE();
             break;
@@ -469,8 +582,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 bit2core", m_stats.m_num_bit2core);
-        st.update("bv->core eq", m_stats.m_num_th2core_eq);
+        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 ackerman", m_stats.m_ackerman);
     }
 
@@ -575,26 +690,40 @@ namespace bv {
         }
     }
 
-    sat::justification solver::mk_bv2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) {
+    sat::justification solver::mk_eq2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) {
         void* mem = get_region().allocate(bv_justification::get_obj_size());
         sat::constraint_base::initialize(mem, this);
         auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2, c, a);
         return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
     }
 
-    sat::ext_justification_idx solver::mk_bit2bv_justification(theory_var v1, theory_var v2) {
+    sat::ext_justification_idx solver::mk_bit2eq_justification(theory_var v1, theory_var v2) {
         void* mem = get_region().allocate(bv_justification::get_obj_size());
         sat::constraint_base::initialize(mem, this);
         auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2);
         return constraint->to_index();
     }
 
+    sat::justification solver::mk_bit2ne_justification(unsigned idx, sat::literal c) {
+        void* mem = get_region().allocate(bv_justification::get_obj_size());
+        sat::constraint_base::initialize(mem, this);
+        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(idx, c);
+        return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+    }
+
+    sat::justification solver::mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a) {
+        void* mem = get_region().allocate(bv_justification::get_obj_size());
+        sat::constraint_base::initialize(mem, this);
+        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(idx, v1, v2, c, a);
+        return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+    }
+
     void solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
         m_stats.m_num_bit2core++;
         SASSERT(ctx.s().value(antecedent) == l_true);
         SASSERT(m_bits[v2][idx].var() == consequent.var());
         SASSERT(consequent.var() != antecedent.var());
-        s().assign(consequent, mk_bv2bit_justification(v1, v2, consequent, antecedent));
+        s().assign(consequent, mk_eq2bit_justification(v1, v2, consequent, antecedent));
         if (s().value(consequent) == l_false) {
             m_stats.m_num_conflicts++;
             SASSERT(s().inconsistent());
@@ -615,7 +744,7 @@ namespace bv {
             if (a && a->is_bit())
                 for (auto curr : a->to_bit())
                     if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx) 
-                        m_prop_queue.push_back(curr);                    
+                        m_prop_queue.push_back(propagation_item(curr));                    
         }
     }
 
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index a70c9d48a4d..76fe5207526 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -43,23 +43,29 @@ namespace bv {
         friend class ackerman;
 
         struct stats {
-            unsigned   m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
+            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_ackerman;
             void reset() { memset(this, 0, sizeof(stats)); }
             stats() { reset(); }
         };
 
         struct bv_justification {
-            enum kind_t { bv2bit, bit2bv };
+            enum kind_t { eq2bit, ne2bit, bit2eq, bit2ne };
             kind_t     m_kind;
-            theory_var m_v1;
-            theory_var m_v2;
+            theory_var m_v1{ euf::null_theory_var };
+            theory_var m_v2 { euf::null_theory_var };
+            unsigned   m_idx{ UINT_MAX };
             sat::literal m_consequent;
             sat::literal m_antecedent;
             bv_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
-                m_kind(kind_t::bv2bit), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
+                m_kind(bv_justification::kind_t::eq2bit), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
             bv_justification(theory_var v1, theory_var v2):
-                m_kind(kind_t::bit2bv), m_v1(v1), m_v2(v2) {}
+                m_kind(bv_justification::kind_t::bit2eq), m_v1(v1), m_v2(v2) {}
+            bv_justification(unsigned idx, sat::literal c) :
+                m_kind(bv_justification::kind_t::bit2ne), m_idx(idx), m_consequent(c) {}
+            bv_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
+                m_kind(bv_justification::kind_t::ne2bit), m_idx(idx), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
             sat::ext_constraint_idx to_index() const { 
                 return sat::constraint_base::mem2base(this); 
             }
@@ -69,8 +75,10 @@ namespace bv {
             static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(bv_justification)); }
         };
 
-        sat::justification mk_bv2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a);
-        sat::ext_justification_idx mk_bit2bv_justification(theory_var v1, theory_var v2);
+        sat::justification mk_eq2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a);
+        sat::ext_justification_idx mk_bit2eq_justification(theory_var v1, theory_var v2);
+        sat::justification mk_bit2ne_justification(unsigned idx, sat::literal c);
+        sat::justification mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a);
         void log_drat(bv_justification const& c);
  
 
@@ -125,13 +133,46 @@ 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;
+            euf::enode* m_node;
+            eq_occurs*  m_next;
+            eq_occurs(unsigned idx, theory_var v1, theory_var v2, euf::enode* n, eq_occurs* next = nullptr):
+                m_idx(idx), m_v1(v1), m_v2(v2), 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 {
             var_pos_occ * m_occs;
-            bit_atom():m_occs(nullptr) {}
+            eq_occurs   * m_eqs;
+            bit_atom():m_occs(nullptr), m_eqs(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(*this); }
         };
 
         struct def_atom : public atom {
@@ -142,8 +183,17 @@ namespace bv {
             bool is_bit() const override { return false; }
         };
 
+        struct propagation_item {
+            var_pos m_vp { var_pos(0, 0) };
+            bit_atom* m_atom{ nullptr };
+            explicit propagation_item(bit_atom* a) : m_atom(a) {}
+            explicit propagation_item(var_pos const& vp) : m_vp(vp) {}            
+        };
+
+
         class bit_trail;
         class add_var_pos_trail;
+        class add_eq_occurs_trail;
         class mk_atom_trail;
         class bit_occs_trail;
         typedef ptr_vector<atom> bool_var2atom;
@@ -160,15 +210,16 @@ namespace bv {
         vector<zero_one_bits>    m_zero_one_bits; // per var, see comment in the struct zero_one_bit
         bool_var2atom            m_bool_var2atom;
         value2var                m_fixed_var_table;
-        mutable vector<rational> m_power2;
-        literal_vector           m_tmp_literals;
-        svector<var_pos>         m_prop_queue;
-        unsigned_vector          m_prop_queue_lim;
-        unsigned                 m_prop_queue_head { 0 };
+        mutable vector<rational>   m_power2;
+        literal_vector             m_tmp_literals;
+        svector<propagation_item>  m_prop_queue;
+        unsigned_vector            m_prop_queue_lim;
+        unsigned                   m_prop_queue_head { 0 };
 
 
         sat::solver* m_solver;
         sat::solver& s() { return *m_solver;  }
+        sat::solver const& s() const { return *m_solver;  }
 
         // internalize
         void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); }
@@ -191,6 +242,8 @@ namespace bv {
         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);
+
         void set_bit_eh(theory_var v, literal l, unsigned idx);
         void init_bits(expr* e, expr_ref_vector const & bits);
         void mk_bits(theory_var v);
@@ -227,10 +280,12 @@ namespace bv {
         bool merge_zero_one_bits(theory_var r1, theory_var r2);
         void 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);
         numeral const& power2(unsigned i) const;
 
         // invariants
         bool check_zero_one_bits(theory_var v);
+        void check_missing_propagation() const;
         void validate_atoms() const;
        
     public:
@@ -282,6 +337,7 @@ namespace bv {
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override { return false; }
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void internalize(expr* e, bool redundant) override;
+        void eq_internalized(euf::enode* n) override;
         euf::theory_var mk_var(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode * n, sort * s) override;
 
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 5bc32013ce3..fd1ba52f493 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -93,6 +93,12 @@ namespace euf {
             if (s_ext && s_ext != e_ext)
                 s_ext->apply_sort_cnstr(n, m.get_sort(e));
         }
+        expr* a = nullptr, * b = nullptr;
+        if (m.is_eq(e, a, b) && m.get_sort(a)->get_family_id() != null_family_id) {
+            auto* s_ext = sort2solver(m.get_sort(a));
+            if (s_ext)
+                s_ext->eq_internalized(n);
+        }
         axiomatize_basic(n);
     }
 
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 416a2388d1b..23dff1f5a3f 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -352,6 +352,7 @@ namespace euf {
             return sat::check_result::CR_CONTINUE;
         if (give_up)
             return sat::check_result::CR_GIVEUP;
+        TRACE("after_search", s().display(tout););
         return sat::check_result::CR_DONE;
     }
 
@@ -390,34 +391,47 @@ namespace euf {
         }
     }
 
+    /**
+    * After a pop has completed, re-initialize the association between Boolean variables 
+    * and the theories by re-creating the expression/variable mapping used for Booleans
+    * and replaying internalization.
+    */
     void solver::finish_reinit() {
-
         SASSERT(s().get_vars_to_reinit().size() == m_reinit_exprs.size());
         if (s().get_vars_to_reinit().empty())
             return;
+
+        struct scoped_set_replay {
+            solver& s;
+            obj_map<expr, sat::bool_var> m;
+            scoped_set_replay(solver& s) :s(s) {
+                s.si.set_expr2var_replay(&m);
+            }
+            ~scoped_set_replay() { 
+                s.si.set_expr2var_replay(nullptr); 
+            }
+        };
+        scoped_set_replay replay(*this);
         unsigned i = 0;
-        obj_map<expr, sat::bool_var> expr2var_replay;
         for (sat::bool_var v : s().get_vars_to_reinit()) {
             expr* e = m_reinit_exprs.get(i++);
-            if (!e)
-                continue;
-            expr2var_replay.insert(e, v);
+            if (e)
+                replay.m.insert(e, v);
         }
-        if (expr2var_replay.empty())
+        if (replay.m.empty())
             return;
-        si.set_expr2var_replay(&expr2var_replay);
-        TRACE("euf", for (auto const& kv : expr2var_replay) tout << "replay: " << kv.m_value << " " << mk_bounded_pp(kv.m_key, m) << "\n";);
-        for (auto const& kv : expr2var_replay) {
+        
+        TRACE("euf", for (auto const& kv : replay.m) tout << "replay: " << kv.m_value << " " << mk_bounded_pp(kv.m_key, m) << "\n";);
+        for (auto const& kv : replay.m) {
             sat::literal lit;
             expr* e = kv.m_key;
             if (si.is_bool_op(e)) 
-                lit = literal(expr2var_replay[e], false);
+                lit = literal(replay.m[e], false);
             else 
                 lit = si.internalize(kv.m_key, true);
             VERIFY(lit.var() == kv.m_value);
             attach_lit(lit, kv.m_key);            
         }
-        si.set_expr2var_replay(nullptr);   
         TRACE("euf", tout << "replay done\n";);
     }
 
@@ -439,9 +453,13 @@ namespace euf {
     }
 
     lbool solver::get_phase(bool_var v) { 
+        TRACE("euf", tout << "phase: " << v << "\n";);            
         auto* ext = bool_var2solver(v);
         if (ext)
             return ext->get_phase(v);
+        expr* e = bool_var2expr(v);
+        if (e && m.is_eq(e))
+            return l_true;
         return l_undef; 
     }
 
@@ -481,14 +499,28 @@ namespace euf {
 
     std::ostream& solver::display_justification_ptr(std::ostream& out, size_t* j) const {
         if (is_literal(j))
-            return out << get_literal(j) << " ";
+            return out << "sat: " << get_literal(j);
         else
-            return display_justification(out, get_justification(j)) << " ";
+            return display_justification(out, get_justification(j));
     }
 
     std::ostream& solver::display_justification(std::ostream& out, ext_justification_idx idx) const { 
         auto* ext = sat::constraint_base::to_extension(idx);
-        if (ext != this)
+        if (ext == this) {
+            constraint& c = constraint::from_idx(idx);
+            switch (c.kind()) {
+            case constraint::kind_t::conflict:
+                return out << "euf conflict";
+            case constraint::kind_t::eq:
+                return out << "euf equality propagation";
+            case constraint::kind_t::lit:
+                return out << "euf literal propagation";
+            default:
+                UNREACHABLE();
+                return out;
+            }                
+        }
+        else 
             return ext->display_justification(out, idx);
         return out; 
     }
@@ -497,7 +529,7 @@ namespace euf {
         auto* ext = sat::constraint_base::to_extension(idx);
         if (ext != this)
             return ext->display_constraint(out, idx);
-        return out; 
+        return display_justification(out, idx);
     }
 
     void solver::collect_statistics(statistics& st) const {
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index 4173bae8ece..e0450cd897b 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -99,7 +99,6 @@ namespace euf {
     }
     
     void th_euf_solver::push_core() {
-        TRACE("euf", tout << "push-core\n";);
         m_var2enode_lim.push_back(m_var2enode.size());
     }
 
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 18d435fe821..eed5d7cb027 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -52,6 +52,11 @@ namespace euf {
         */
         virtual void apply_sort_cnstr(enode * n, sort * s) {}
 
+        /**
+           \record that an equality has been internalized.
+         */
+        virtual void eq_internalized(enode* n) {}
+
     };
 
     class th_decompile {
@@ -138,7 +143,10 @@ namespace euf {
 
         virtual void push_core();
         virtual void pop_core(unsigned n);
-        void force_push() { for (; m_num_scopes > 0; --m_num_scopes) push_core(); }
+        void force_push() { 
+            CTRACE("euf", m_num_scopes > 0, tout << "push-core " << m_num_scopes << "\n";);
+            for (; m_num_scopes > 0; --m_num_scopes) push_core(); 
+        }
 
     public:
         th_euf_solver(euf::solver& ctx, euf::theory_id id);
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 12228e8a58a..59fba823cc7 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -669,13 +669,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     struct scoped_stack {
+        imp& i;
         sat::literal_vector& r;
         unsigned rsz;
         svector<frame>& frames;
         unsigned fsz;
         bool is_root;
         scoped_stack(imp& x, bool is_root) :
-            r(x.m_result_stack), rsz(r.size()), frames(x.m_frame_stack), fsz(frames.size()), is_root(is_root)
+            i(x), r(i.m_result_stack), rsz(r.size()), frames(x.m_frame_stack), fsz(frames.size()), is_root(is_root)
         {}
         ~scoped_stack() {
             if (frames.size() > fsz) {
@@ -683,9 +684,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 r.shrink(rsz);
                 return;
             }
-            SASSERT(frames.size() == fsz);
-            SASSERT(!is_root || rsz == r.size());
-            SASSERT(is_root || rsz + 1 == r.size());
+            SASSERT(i.m.limit().is_canceled() || frames.size() == fsz);
+            SASSERT(i.m.limit().is_canceled() || !is_root || rsz == r.size());
+            SASSERT(i.m.limit().is_canceled() || is_root || rsz + 1 == r.size());
         }
     };
 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 20f931e7e46..a5d8e6caf26 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3854,6 +3854,7 @@ namespace smt {
                 TRACE("final_check_result", tout << "fcs: " << fcs << " last_search_failure: " << m_last_search_failure << "\n";);
                 switch (fcs) {
                 case FC_DONE:
+                    log_stats();
                     return l_true;
                 case FC_CONTINUE:
                     break;
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 6fa32f3fa7e..6b7db2d8fc9 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1178,6 +1178,12 @@ namespace smt {
             literal arg = ctx.get_literal(diff);
             lits.push_back(arg);
         }
+        TRACE("bv", 
+              tout << mk_pp(get_enode(v1)->get_owner(), m) << " = " << mk_pp(get_enode(v2)->get_owner(), m) << " " 
+              << ctx.get_scope_level() 
+              << "\n";
+              ctx.display_literals_smt2(tout, lits););
+
         m_stats.m_num_diseq_dynamic++;
         scoped_trace_stream st(*this, lits);
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());