diff --git a/src/sat/smt/bv_invariant.cpp b/src/sat/smt/bv_invariant.cpp
index 1178ed105..c73c9806d 100644
--- a/src/sat/smt/bv_invariant.cpp
+++ b/src/sat/smt/bv_invariant.cpp
@@ -93,8 +93,16 @@ namespace bv {
         } while (curr != v);
 
         zero_one_bits const& _bits = m_zero_one_bits[v];
-        if (_bits.size() != num_bits)
-            std::cout << v << " " << _bits.size() << " " << num_bits << "\n";
+        if (_bits.size() != num_bits) {
+            std::cout << "v" << v << " " << _bits.size() << " " << num_bits << "\n";
+            std::cout << "true: " << mk_true() << "\n";
+            do {
+                std::cout << "v" << curr << ": " << m_bits[curr] << "\n";
+                curr = m_find.next(curr);
+            }
+            while (curr != v);
+        }
+        SASSERT(_bits.size() == num_bits);
         VERIFY(_bits.size() == num_bits);
         bool_vector already_found;
         already_found.resize(bv_sz, false);
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 35ea2e104..3a35a73d5 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -664,7 +664,7 @@ namespace bv {
         result->set_solver(&ctx.s());
         for (theory_var i = 0; i < static_cast<theory_var>(get_num_vars()); ++i)
             if (find(i) != i)
-                result->m_find.merge(i, find(i));
+                result->m_find.set_root(i, find(i));
         result->m_prop_queue.append(m_prop_queue);
         for (unsigned i = 0; i < m_bool_var2atom.size(); ++i) {
             atom* a = m_bool_var2atom[i];
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index 94f0b03dc..4bb65c995 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -102,6 +102,9 @@ namespace bv {
             unsigned   m_is_true:1;
             zero_one_bit(theory_var v = euf::null_theory_var, unsigned idx = UINT_MAX, bool is_true = false):
                 m_owner(v), m_idx(idx), m_is_true(is_true) {}
+            std::ostream& display(std::ostream& out) const {
+                return out << "v" << m_owner << " @ " << m_idx << " " << (m_is_true?"T":"F");
+            }
         };
 
         typedef svector<zero_one_bit> zero_one_bits;
@@ -367,9 +370,12 @@ namespace bv {
         typedef std::pair<solver const*, theory_var> pp_var;
         pp_var pp(theory_var v) const { return pp_var(this, v); }
 
+        friend std::ostream& operator<<(std::ostream& out, solver::zero_one_bit const& zo) { return zo.display(out); }
+
     };
 
     inline std::ostream& operator<<(std::ostream& out, solver::pp_var const& p) { return p.first->display(out, p.second); }
 
 
+
 }
diff --git a/src/util/union_find.h b/src/util/union_find.h
index cd487a007..664efefda 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -134,6 +134,14 @@ public:
         CASSERT("union_find", check_invariant());
     }
 
+    void set_root(unsigned v, unsigned root) {
+        TRACE("union_find", tout << "merging " << v << " " << root << "\n";);
+        SASSERT(v != root);
+        m_find[v] = root;
+        m_size[root] += m_size[v];
+        std::swap(m_next[root], m_next[v]);
+    }
+
     // dissolve equivalence class of v
     // this method cannot be used with backtracking.
     void dissolve(unsigned v) {