diff --git a/src/muz/ddnf/doc.cpp b/src/muz/ddnf/doc.cpp
index 7968f55be..4c12b4bee 100644
--- a/src/muz/ddnf/doc.cpp
+++ b/src/muz/ddnf/doc.cpp
@@ -22,7 +22,7 @@ Revision History:
 
 #include "doc.h"
 
-doc_manager::doc_manager(unsigned n): m(n) {
+doc_manager::doc_manager(unsigned n): m(n), m_alloc("doc") {
     m_full = m.allocateX();
 }
 
@@ -30,39 +30,43 @@ doc_manager::~doc_manager() {
     m.deallocate(m_full);
 }
 
-void doc_manager::reset() {
-    // m.reset(); - not until docs are in small object allocator.
-}
 doc* doc_manager::allocate() {
-    return alloc(doc, m.allocate());
+    return allocate(m.allocate());
 }
 doc* doc_manager::allocate1() {
-    return alloc(doc, m.allocate1());
+    return allocate(m.allocate1());
 }
 doc* doc_manager::allocate0() {
-    return alloc(doc, m.allocate0());
+    return allocate(m.allocate0());
 }
 doc* doc_manager::allocateX() {
-    return alloc(doc, m.allocateX());
+    return allocate(m.allocateX());
 }
 doc* doc_manager::allocate(doc const& src) {
-    doc* r = alloc(doc, m.allocate(src.pos()));
+    doc* r = allocate(m.allocate(src.pos()));
     for (unsigned i = 0; i < src.neg().size(); ++i) {
         r->neg().push_back(m.allocate(src.neg()[i]));
     }
     return r;
 }
+doc* doc_manager::allocate(tbv* t) {
+    void* mm = m_alloc.allocate(sizeof(doc));
+    return new (mm) doc(t);
+}
+doc* doc_manager::allocate(tbv const& src) {
+    return allocate(m.allocate(src));
+}
 doc* doc_manager::allocate(uint64 n) {
-    return alloc(doc, m.allocate(n));
+    return allocate(m.allocate(n));
 }
 doc* doc_manager::allocate(rational const& r) {
-    return alloc(doc, m.allocate(r));
+    return allocate(m.allocate(r));
 }
 doc* doc_manager::allocate(uint64 n, unsigned hi, unsigned lo) {
-    return alloc(doc, m.allocate(n, hi, lo));
+    return allocate(m.allocate(n, hi, lo));
 }
 doc* doc_manager::allocate(doc const& src, unsigned const* permutation) {
-    doc* r = alloc(doc, m.allocate(src.pos(), permutation));
+    doc* r = allocate(m.allocate(src.pos(), permutation));
     for (unsigned i = 0; i < src.neg().size(); ++i) {
         r->neg().push_back(m.allocate(src.neg()[i], permutation));
     }
@@ -72,7 +76,8 @@ void doc_manager::deallocate(doc* src) {
     if (!src) return;
     m.deallocate(&src->pos());
     src->neg().reset(m);
-    dealloc(src);
+    m_alloc.deallocate(sizeof(doc), src);
+    //    dealloc(src);
 }
 void doc_manager::copy(doc& dst, doc const& src)  {
     m.copy(dst.pos(), src.pos());
@@ -105,11 +110,31 @@ doc& doc_manager::fillX(doc& src) {
 bool doc_manager::set_and(doc& dst, doc const& src)  {
     // (A \ B) & (C \ D) = (A & C) \ (B u D)
     if (!m.set_and(dst.pos(), src.pos())) return false;
+    for (unsigned i = 0; i < dst.neg().size(); ++i) {
+        if (!m.set_and(dst.neg()[i], dst.pos())) {
+            dst.neg().erase(m, i);
+            --i;
+        }
+    }
+    tbv_ref t(m);
     for (unsigned i = 0; i < src.neg().size(); ++i) {
-        dst.neg().insert(m, m.allocate(src.neg()[i]));
+        t = m.allocate(src.neg()[i]);
+        if (m.set_and(*t, dst.pos())) {
+            dst.neg().insert(m, t.detach());
+        }
     }
     return (src.neg().is_empty() || fold_neg(dst));
 }
+
+bool doc_manager::well_formed(doc const& d) const {
+    if (!m.is_well_formed(d.pos())) return false;
+    for (unsigned i = 0; i < d.neg().size(); ++i) {
+        if (!m.is_well_formed(d.neg()[i])) return false;
+        if (!m.contains(d.pos(), d.neg()[i])) return false;
+    }
+    return true;
+}
+
 bool doc_manager::fold_neg(doc& dst) {
  start_over:
     for (unsigned i = 0; i < dst.neg().size(); ++i) {
@@ -153,143 +178,239 @@ unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& inde
     }
     return count;
 }
-doc* doc_manager::project(unsigned n, bool const* to_delete, doc const& src) {
-    tbv* p = tbvm().project(n, to_delete, src.pos());
-    if (src.neg().is_empty()) {
-        // build doc from p.
-        return 0;
+
+void doc_manager::set(doc& d, unsigned idx, tbit value) {
+    d.pos().set(idx, value);
+    for (unsigned i = 0; i < d.neg().size(); ++i) {
+        d.neg()[i].set(idx, value);
     }
-    NOT_IMPLEMENTED_YET();
-    ptr_vector<tbv> todo;
-#if 0
-    // tbv & ~tbv1 & ~tbv2 & ..
-    // Semantics of ~tbv1 is that it is a clause of literals.
-    //   indices where BIT_1 is set are negative.
-    //   indices where BIT_0 is set are positive.
-    // The first loop is supposed to project tbv_i directly
-    // when some safety condition is met.
-    // The second loop handles the remaining tbv_i that
-    // don't meet the safety condition.
-    for (unsigned i = 0; i < src.neg().size(); ++i) {
-        if (can_project_neg(n, to_delete, src.neg()[i])) {
-            
-        }
+}
+
+//
+// merge range from [lo:lo+length-1] with each index in equivalence class.
+// under assumption of equalities and columns that are discarded.
+//
+bool doc_manager::merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols) {
+    for (unsigned i = 0; i < length; ++i) {
+        unsigned idx = lo + i;
+        if (!merge(d, lo + i, equalities, discard_cols)) return false;
     }
-#endif
-#if 0
-    // REVIEW: what is the spec for this code?
-    ternary_diff_bitvector TBV(*this);
-    if (!TBV.fold_neg())
-        return false;
-    
-    std::set<ternary_bitvector*> todo;
-    cpy_bits_t cpy_bits;
-    ternary_bitvector newneg;
-    for (union_ternary_bitvector<ternary_bitvector>::iterator I = TBV.m_neg.begin(),
-             E = TBV.m_neg.end(); I != E; ++I) {
-        // check if subtract TBV should be skiped
-        for (unsigned i = 0; i < delcols.size()-1; ++i) {
-            unsigned idx = delcols[i];
-            if (I->get(idx) != TBV.m_pos.get(idx)) { // xx \ 1x
-                if (analyze_copy_bit(TBV.m_pos, *I, delcols, cpy_bits))
-                    todo.insert(&*I);
-                goto skip_row;
+    return true;
+}
+bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols) {
+    unsigned root = equalities.find(idx);
+    idx = root;
+    unsigned num_x = 0;
+    unsigned root1;
+    tbit value = BIT_x;
+    do {
+        switch (d[idx]) {
+        case BIT_0:
+            if (value == BIT_1) return false;
+            value = BIT_0;
+            break;
+        case BIT_1:
+            if (value == BIT_0) return false;
+            value = BIT_1;
+            break;
+        case BIT_x:
+            if (!discard_cols.get(idx)) {
+                ++num_x;
+                root1 = idx;
             }
+            break;
+        default:
+            break;
         }
-        
-        newneg.reset();
-        I->project(delcols, new_size, newneg);
-        result.m_neg.add_fact(newneg);
-    skip_row:   ;
+        idx = equalities.next(idx);
+    }
+    while (idx != root);
+
+    if (num_x == 0) {
+        // nothing to do.
+    }
+    else if (value != BIT_x) {
+        do {
+            if (d[idx] == BIT_x) {
+                set(d, idx, value);
+            }
+            idx = equalities.next(idx);
+        }
+        while (idx != root);
+    }
+    else {
+        do {
+            if (!discard_cols.get(idx) && idx != root1) {
+                tbv* t = tbvm().allocate(d.pos());
+                t->set(idx, BIT_0);
+                t->set(root1, BIT_1);
+                d.neg().insert(tbvm(), t);
+                t = tbvm().allocate(d.pos());
+                t->set(idx, BIT_1);
+                t->set(root1, BIT_0);
+                d.neg().insert(tbvm(), t);                
+            }
+            idx = equalities.next(idx);
+        }
+        while (idx != root);
+    }
+    return true;
+}
+
+//
+// 1. If n = 0,1: can project directly.
+// 2. If tbv_i uses X in all positions with vars or constant where tbv is constant: can project directly.
+// 3. Perform resolution on remaining tbv_i 
+//
+// tbv & ~tbv1 & ~tbv2 & .. & ~tbv_n
+// Semantics of ~tbv1 is that it is a clause of literals.
+//   indices where BIT_1 is set are negative.
+//   indices where BIT_0 is set are positive.
+//
+
+doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) {
+    tbv_manager& dstt = dstm.m;
+    doc* r = dstm.allocate(dstt.project(n, to_delete, src.pos()));
+
+    if (src.neg().is_empty()) {
+        return r;
+    }
+    if (src.neg().size() == 1) {
+        r->neg().push_back(dstt.project(n, to_delete, src.neg()[0]));
+        return r;
     }
     
-    if (!todo.empty()) {
-        for (std::set<ternary_bitvector*>::iterator I = todo.begin(),
-                 E = todo.end(); I != E; ++I) {
-            for (unsigned i = 0; i < delcols.size()-1; ++i) {
-                unsigned idx = delcols[i];
-                if ((*I)->get(idx) != TBV.m_pos.get(idx)) {
-                    cpy_bits_t::iterator II = cpy_bits.find(idx);
-                    if (II == cpy_bits.end())
-                        goto skip_bv;
-                    
-                    unsigned idx_keep = II->second.first;
-                    unsigned cpy_val = II->second.second;
-                    
-                    if (!((*I)->get(idx) & cpy_val) || (*I)->get(idx_keep) != BIT_x)
-                        goto skip_bv;
-                    
-                    (*I)->set(idx_keep, (*I)->get(idx));
+    //
+    // All negations can be projected if they are sign compatible.
+    //
+    tbv_ref bits(tbvm(), tbvm().allocateX());
+    for (unsigned i = 0; i < src.neg().size(); ++i) {        
+        tbvm().set_and(*bits, src.neg()[i]);
+    }
+    bool can_project_const = true;
+    for (unsigned i = 0; can_project_const && i < n; ++i) {
+        can_project_const = !to_delete[i] || (*bits)[i] == BIT_x;
+    }
+    if (can_project_const) {
+        for (unsigned i = 0; i < src.neg().size(); ++i) {        
+            r->neg().push_back(dstt.project(n, to_delete, src.neg()[i]));
+        }
+        return r;
+    }
+
+    // 
+    // A negation can be projected directly if it does not constrain
+    // deleted variables.
+    // 
+    ptr_vector<tbv> todo;
+    for (unsigned i = 0; i < src.neg().size(); ++i) {        
+        if (can_project_neg(src.pos(), n, to_delete, src.neg()[i])) {
+            r->neg().push_back(dstt.project(n, to_delete, src.neg()[i]));
+        }
+        else {
+            todo.push_back(tbvm().allocate(src.neg()[i]));
+        }
+    }
+    if (todo.empty()) {
+        return r;
+    }
+    ptr_vector<tbv> pos, neg, new_todo;
+    tbv_ref t1(tbvm()), t2(tbvm());
+    for (unsigned i = 0; i < n; ++i) {
+        if (to_delete[i] && (*bits)[i] != BIT_x) {
+            TRACE("doc", tout << "delete " << i << " ";
+                  for (unsigned j = 0; j < todo.size(); ++j) {
+                      tbvm().display(tout, *todo[j]) << " ";
+                  }
+                  tout << "\n";);
+            new_todo.reset();
+            pos.reset();
+            neg.reset();
+            for (unsigned j = 0; j < todo.size(); ++j) {
+                tbv& t = *todo[j];
+                switch(t[i]) {
+                case BIT_x: new_todo.push_back(&t); break;
+                case BIT_0: neg.push_back(&t); break;
+                case BIT_1: pos.push_back(&t); break;
+                default: UNREACHABLE(); break;                    
                 }
             }
-            
-            newneg.reset();
-            (*I)->project(delcols, new_size, newneg);
-            result.m_neg.add_fact(newneg);
-        skip_bv:        ;
+            if (pos.empty() || neg.empty()) {
+                std::swap(new_todo, todo);
+                continue;
+            }
+            TRACE("doc",
+                  tout << "pos: ";
+                  for (unsigned i = 0; i < pos.size(); ++i) {
+                      tbvm().display(tout, *pos[i]) << " ";
+                  }
+                  tout << "\nneg: ";
+                  for (unsigned i = 0; i < neg.size(); ++i) {
+                      tbvm().display(tout, *neg[i]) << " ";
+                  }
+                  tout << "\n";
+                  );
+                  
+            for (unsigned j = 0; j < pos.size(); ++j) {
+                for (unsigned k = 0; k < neg.size(); ++k) {
+                    t1 = tbvm().allocate(*pos[j]);
+                    (*t1).set(i, BIT_x);
+                    if (tbvm().set_and(*t1, *neg[k])) {
+                        (*t1).set(i, BIT_x);
+                        new_todo.push_back(t1.detach());
+                    }
+                }                
+            }
+            for (unsigned i = 0; i < pos.size(); ++i) {
+                tbvm().deallocate(pos[i]);
+            }
+            for (unsigned i = 0; i < neg.size(); ++i) {
+                tbvm().deallocate(neg[i]);
+            }
+            std::swap(todo, new_todo);
         }
     }
-
-    return !result.is_empty();
-
-
-    // idx_del -> <idx_keep, val>
-    // val -> BIT_*
-    typedef std::map<unsigned, std::pair<unsigned, unsigned char> > cpy_bits_t;
-
-    static bool analyze_copy_bit(const ternary_bitvector& pos, const ternary_bitvector& neg,
-                                 const unsigned_vector& delcols, cpy_bits_t& cpy_bits) {
-      unsigned *del = delcols.c_ptr();
-      bool got_del_col = false, got_keep_col = false;
-      unsigned del_col = 0, keep_col = 0;
-
-      for (unsigned i = 0; i < pos.size(); ++i) {
-        if (pos.get(i) != neg.get(i)) {
-          if (*del == i) {
-            if (got_del_col)
-              return true;
-            del_col = i;
-            got_del_col = true;
-          } else {
-            if (got_keep_col)
-              return true;
-            keep_col = i;
-            got_keep_col = true;
-          }
-        }
-
-        if (i == *del)
-          ++del;
-      }
-
-      if (!got_del_col || !got_keep_col)
-        return true;
-      if (neg.get(keep_col) == neg.get(del_col))
-        return false;
-
-
-      unsigned char val = neg.get(del_col);
-      cpy_bits_t::iterator I = cpy_bits.find(del_col);
-      if (I == cpy_bits.end())
-          cpy_bits[del_col] = std::make_pair(keep_col, val);
-      else {
-          // FIXME: eq classes with size > 1 not supported for now
-          SASSERT(I->second.first == keep_col);
-          I->second.second |= val;
-      }
-
-      return false;
+    for (unsigned i = 0; i < todo.size(); ++i) {
+        r->neg().push_back(dstt.project(n, to_delete, *todo[i]));
+        tbvm().deallocate(todo[i]);
     }
-
-#endif
-    return 0;
+    return r;
 }
 
+bool doc_manager::can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg) {
+    for (unsigned i = 0; i < n; ++i) {
+        if (to_delete[i] && BIT_x != neg[i] && BIT_x == pos[i]) return false;
+    }
+    return true;
+}
+    
+
 void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
-    NOT_IMPLEMENTED_YET();
+    result.reset();
+    if (is_full(src)) {
+        return;
+    }
+    doc* r = allocateX();
+    r->neg().push_back(m.allocate(src.pos()));
+    result.push_back(r);
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        result.push_back(allocate(src.neg()[i]));
+    }
 }
 void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result) {
-    NOT_IMPLEMENTED_YET();
+    doc_ref r(*this), r2(*this);
+    r = allocate(A);
+    if (r->neg().insert(m, m.allocate(B.pos()))) {
+        result.push_back(r.detach());
+        r = allocate(A);
+    }
+    for (unsigned i = 0; i < B.neg().size(); ++i) {
+        r2 = allocate(B.neg()[i]);
+        if (set_and(*r, *r2)) {
+            result.push_back(r.detach());
+            r = allocate(A);
+        }
+    }
 }
 bool doc_manager::equals(doc const& a, doc const& b) const {
     if (!m.equals(a.pos(), b.pos())) return false;
diff --git a/src/muz/ddnf/doc.h b/src/muz/ddnf/doc.h
index e85d6f74a..4a4841dae 100644
--- a/src/muz/ddnf/doc.h
+++ b/src/muz/ddnf/doc.h
@@ -29,20 +29,23 @@ Revision History:
 
 class doc;
 template<typename M, typename T> class union_bvec;
+typedef union_find<> subset_ints;
 
 class doc_manager {
     tbv_manager m;
     tbv*        m_full;
+    small_object_allocator m_alloc;
 public:
     doc_manager(unsigned num_bits);
     ~doc_manager();
     tbv_manager& tbvm() { return m; }
-    void reset();
     doc* allocate();
     doc* allocate1();
     doc* allocate0();
     doc* allocateX();
     doc* allocate(doc const& src);
+    doc* allocate(tbv const& src);
+    doc* allocate(tbv * src);
     doc* allocate(uint64 n);
     doc* allocate(rational const& r);
     doc* allocate(uint64 n, unsigned hi, unsigned lo);
@@ -64,12 +67,16 @@ public:
     bool contains(doc const& a, doc const& b) const;
     std::ostream& display(std::ostream& out, doc const& b) const;
     unsigned num_tbits() const { return m.num_tbits(); }
-    doc* project(unsigned n, bool const* to_delete, doc const& src);
+    doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src);
+    bool well_formed(doc const& d) const;
+    bool merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols);
+    void set(doc& d, unsigned idx, tbit value);
 private:
     unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
+    bool merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols);
+    bool can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg);
 };
 
-typedef union_find<> subset_ints;
 
 // union of tbv*, union of doc*
 template<typename M, typename T>
@@ -210,98 +217,31 @@ public:
             push_back(m.allocate(other[i]));
         }
     }
-    void fix_eq_bits(unsigned idx1, tbv* BV, unsigned idx2, unsigned length,
-                     subset_ints& equalities, const bit_vector& discard_cols) {
-        for (unsigned i = 0; i < length; ++i) {
-            unsigned k = 0;
-            for (unsigned j = 0; j < size(); ++j, ++k) {
-                NOT_IMPLEMENTED_YET();
 
-#if 0
-                T *eqBV = BV ? const_cast<T*>(BV) : &*I;
-                bool discard_col = discard_cols.get(idx1+i) || (!BV && discard_cols.get(idx2+i));
-                
-                switch (fix_single_bit(*I, idx1+i, eqBV, idx2+i, equalities, discard_col)) {
-                case 1:
-                    // remove row
-                    I = m_bitvectors.erase(I);
-                    break;
-                    
-                case 2: {
-                    // don't care column equality. try subtraction first.
-                    union_ternary_bitvector diff(I->size()), result(I->size());
-                    T BV(I->size(), true);
-                    BV.set(idx1+i, BIT_0);
-                    BV.set(idx2+i, BIT_1);
-                    diff.add_new_fact(BV);
-                    
-                    BV.set(idx1+i, BIT_1);
-                    BV.set(idx2+i, BIT_0);
-                    diff.add_new_fact(BV);
-                    
-                    I->subtract(diff, result);
-                    *I = *result.begin();
-                    ++I;
-                    break;
-                }
-
-                default:
-                    if (I->is_empty()) {
-                        I = m_bitvectors.erase(I);
-                    } else {
-                        // bits fixed
-                        ++I;
-                    }
-                }
-#endif
+    void merge(M& m, unsigned lo, unsigned length, subset_ints & equalities, bit_vector const& discard_cols) {
+        for (unsigned i = 0; i < size(); ++i) {
+            if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) {
+                erase(m, i);
+                --i;
             }
         }
     }
 
+    void merge(M& m, unsigned lo1, unsigned lo2, unsigned length, bit_vector const& discard_cols) {
+        union_find_default_ctx union_ctx;
+        subset_ints equalities(union_ctx);
+        for (unsigned i = 0; i < discard_cols.size(); ++i) {
+            equalities.mk_var();
+        }
+        for (unsigned j = 0; j < length; ++j) {
+            equalities.merge(lo1 + j, lo2 + j);
+        }
+        merge(m, lo1, length, equalities, discard_cols);
+    }
+
+
 private:
 
-    fix_bit_result_t fix_single_bit(tbv& bv, unsigned idx, unsigned value, const subset_ints& equalities) {
-        unsigned root = equalities.find(idx);
-        idx = root;
-        do {
-            unsigned bitval = bv.get(idx);
-            if (bitval == tbv::BIT_x) {
-                bv.set(idx, value);
-            } 
-            else if (bitval != value) {
-                return e_row_removed;
-            }
-            idx = equalities.next(idx);
-        } 
-        while (idx != root);
-        return e_fixed;
-    }
-
-    fix_bit_result_t fix_single_bit(tbv & BV1, unsigned idx1, tbv & BV2, unsigned idx2,
-                                  subset_ints& equalities, bool discard_col) {
-        unsigned A = BV1.get(idx1);
-        unsigned B = BV2.get(idx2);
-        
-        if (A == tbv::BIT_x) {
-            if (B == tbv::BIT_x) {
-                // Both are don't cares.
-                if (!discard_col)
-                    return e_duplicate_row;
-                equalities.merge(idx1, idx2);
-                return e_fixed;
-            } else {
-                // only A is don't care.
-                return fix_single_bit(BV1, idx1, B, equalities);
-            }
-        } else if (B == tbv::BIT_x) {
-            // Only B is don't care.
-            return fix_single_bit(BV2, idx2, A, equalities);
-        } else if (A == B) {
-            return e_fixed;
-        } else {
-            return e_row_removed;
-        }
-    }
 
 };
 
@@ -335,7 +275,7 @@ public:
     utbv& neg() { return m_neg; }
     tbv const& pos() const { return *m_pos; }
     utbv const& neg() const { return m_neg; }
-        
+    tbit operator[](unsigned idx) const { return pos()[idx]; }        
 };
 
 typedef union_bvec<doc_manager, doc> udoc;
@@ -356,6 +296,7 @@ public:
     }
     doc& operator*() { return *d; }
     doc* operator->() { return d; }
+    doc* detach() { doc* r = d; d = 0; return r; }
 };
 
 #endif /* _DOC_H_ */
diff --git a/src/muz/ddnf/tbv.cpp b/src/muz/ddnf/tbv.cpp
index 371233590..e9c04d139 100644
--- a/src/muz/ddnf/tbv.cpp
+++ b/src/muz/ddnf/tbv.cpp
@@ -19,12 +19,26 @@ Revision History:
 --*/
 
 #include "tbv.h"
+#include "hashtable.h"
+
+
+tbv_manager::~tbv_manager() {    
+#if 0
+    ptr_vector<tbv>::iterator it = allocated_tbvs.begin(), end = allocated_tbvs.end();
+    for (; it != end; ++it) {
+        std::cout << "dangling: " << (*it) << "\n";
+    }
+#endif
+}
 
 void tbv_manager::reset() {
     m.reset();
 }
 tbv* tbv_manager::allocate() {
-    return reinterpret_cast<tbv*>(m.allocate());
+    tbv* r = reinterpret_cast<tbv*>(m.allocate());
+    //std::cout << allocated_tbvs.size() << " " << r << "\n";
+    //allocated_tbvs.insert(r);
+    return r;
 }
 tbv* tbv_manager::allocate1() {
     tbv* v = allocate();
@@ -42,7 +56,9 @@ tbv* tbv_manager::allocateX() {
     return v;
 }
 tbv* tbv_manager::allocate(tbv const& bv) {
-    return reinterpret_cast<tbv*>(m.allocate(bv));
+    tbv* r = allocate();
+    copy(*r, bv);
+    return r;
 }
 tbv* tbv_manager::allocate(uint64 val) {
     tbv* v = allocate0();
@@ -124,6 +140,13 @@ tbv* tbv_manager::allocate(rational const& r) {
     return v;
 }
 void tbv_manager::deallocate(tbv* bv) {
+#if 0
+    if (!allocated_tbvs.contains(bv)) {
+        std::cout << "double deallocate: " << bv << "\n";
+        UNREACHABLE();
+    }
+    allocated_tbvs.erase(bv);
+#endif
     m.deallocate(bv);
 }    
 void tbv_manager::copy(tbv& dst, tbv const& src) const {
@@ -150,8 +173,12 @@ tbv& tbv_manager::set_or(tbv& dst,  tbv const& src) const {
 }
 bool tbv_manager::set_and(tbv& dst,  tbv const& src) const {
     m.set_and(dst, src); 
+    return is_well_formed(dst);
+}
+
+bool tbv_manager::is_well_formed(tbv const& dst) const {
     for (unsigned i = 0; i < num_tbits(); ++i) {
-        if (dst.get(i) == BIT_z) return false;
+        if (dst[i] == BIT_z) return false;
     }
     return true;
 }
diff --git a/src/muz/ddnf/tbv.h b/src/muz/ddnf/tbv.h
index bbe993b21..05584e391 100644
--- a/src/muz/ddnf/tbv.h
+++ b/src/muz/ddnf/tbv.h
@@ -40,8 +40,10 @@ inline tbit neg(tbit t) {
 class tbv_manager {
     friend class tbv;
     fixed_bit_vector_manager m;
+    //    ptr_vector<tbv> allocated_tbvs;
 public:
     tbv_manager(unsigned n): m(2*n) {}
+    ~tbv_manager();
     void reset();
     tbv* allocate();
     tbv* allocate1();
@@ -70,6 +72,7 @@ public:
     bool intersect(tbv const& a, tbv const& b, tbv& result);
     std::ostream& display(std::ostream& out, tbv const& b) const;
     tbv* project(unsigned n, bool const* to_delete, tbv const& src);
+    bool is_well_formed(tbv const& b) const; // - does not contain BIT_z;
 };
 
 class tbv: private fixed_bit_vector {
@@ -130,6 +133,7 @@ public:
     }
     tbv& operator*() { return *d; }
     tbv* get() { return d; }
+    tbv* detach() { tbv* result = d; d = 0; return result; }
 };
 
 
diff --git a/src/muz/ddnf/udoc_relation.cpp b/src/muz/ddnf/udoc_relation.cpp
index 34156c2c7..9c63e7fd5 100644
--- a/src/muz/ddnf/udoc_relation.cpp
+++ b/src/muz/ddnf/udoc_relation.cpp
@@ -461,14 +461,18 @@ namespace datalog {
             for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) {
                 m_equalities.mk_var();
             }
+            for (unsigned i = 1; i < col_cnt; ++i) {
+                for (unsigned j = 0; j < m_size; ++j) {
+                    m_equalities.merge(m_cols[0]+j ,m_cols[i]+j);
+                }
+            }
         }
         
         virtual void operator()(relation_base & _r) {
             udoc_relation& r = get(_r);
             udoc& d = r.get_udoc();
-            for (unsigned i = 1; i < m_cols.size(); ++i) {
-                d.fix_eq_bits(m_cols[0], 0, m_cols[i], m_size, m_equalities, m_empty_bv);
-            }
+            doc_manager& dm = r.get_dm();
+            d.merge(dm, m_cols[0], m_size, m_equalities, m_empty_bv);
             TRACE("dl", tout << "final size: " << r.get_size_estimate_rows() << '\n';);
         }
     };
@@ -624,10 +628,10 @@ namespace datalog {
             SASSERT(m.is_bool(g));
             unsigned v = to_var(g)->get_idx();
             unsigned idx = column_idx(v);
-            doc_manager& dm1 = get_plugin().dm(1);
-            tbv_ref bit1(dm1.tbvm());
-            bit1 = dm1.tbvm().allocate1();
-            result.fix_eq_bits(idx, bit1.get(), 0, 1, equalities, discard_cols);
+            doc_ref d(dm);
+            d = dm.allocateX();
+            dm.set(*d, idx, BIT_1);
+            result.intersect(dm, *d);
         }
         else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
             unsigned hi, lo;
@@ -650,7 +654,7 @@ namespace datalog {
                 unsigned idx1 = column_idx(v1->get_idx());
                 unsigned idx2 = column_idx(v2->get_idx());
                 unsigned length = column_num_bits(v1->get_idx());
-                result.fix_eq_bits(idx1, 0, idx2, length, equalities, discard_cols);
+                result.merge(dm, idx1, idx2, length, discard_cols);
             }   
             else {
                 goto failure_case;
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index e16860b55..f6ebd1e0b 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -9,14 +9,13 @@
 #include "model_smt2_pp.h"
 #include "smt_params.h"
 #include "ast_util.h"
+#include "expr_safe_replace.h"
+#include "th_rewriter.h"
 
 
 static void tst_doc1(unsigned n) {
     doc_manager m(n);
     
-    m.allocate();
-    m.reset();
-
     doc_ref d(m, m.allocate());
     doc_ref d1(m, m.allocate1());
     doc_ref d0(m, m.allocate0());
@@ -74,17 +73,25 @@ static void tst_doc1(unsigned n) {
     m.display(std::cout, *d1) << "\n";
 
 
-#if 0
     svector<bool> to_delete(n, false);
     to_delete[1] = true;
     to_delete[3] = true;
     doc_manager m1(n-2);
-    doc_ref d1_1(m1, m1.project(n, to_delete.c_ptr(), *d0));
+    doc_ref d1_1(m1, m.project(m1, n, to_delete.c_ptr(), *d1));
     doc_ref d1_2(m1, m1.allocate1());
     m.display(std::cout, *d1) << " -> ";
     m1.display(std::cout, *d1_1) << "\n";
     SASSERT(m1.equals(*d1_1,*d1_2));
-#endif
+    m.set(*d1,2,BIT_x);
+    m.set(*d1,4,BIT_x);
+    d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
+    m.display(std::cout, *d1) << " -> ";
+    m1.display(std::cout, *d1_1) << "\n";
+    d1->neg().push_back(m.tbvm().allocate1());
+    SASSERT(m.well_formed(*d1));
+    d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
+    m.display(std::cout, *d1) << " -> ";
+    m1.display(std::cout, *d1_1) << "\n";    
 }
 
 
@@ -106,48 +113,113 @@ class test_doc_project {
         default : return BIT_x;
         }
     }
-    void mk_clause(expr_ref& result, tbv& t) {
-        expr_ref_vector clause(m);
+    expr_ref mk_conj(tbv& t) {
+        expr_ref result(m);
+        expr_ref_vector conjs(m);
         for (unsigned i = 0; i < m_vars.size(); ++i) {
             tbit b = choose_tbit();
             t.set(i, b);            
             switch (b) {
-            case BIT_0: clause.push_back(m.mk_not(m_vars[i].get())); break;
-            case BIT_1: clause.push_back(m_vars[i].get()); break;
+            case BIT_1: conjs.push_back(m_vars[i].get()); break;
+            case BIT_0: conjs.push_back(m.mk_not(m_vars[i].get())); break;
             default: break;
             }
         }
-        result = mk_or(m, clause.size(), clause.c_ptr());
+        result = mk_and(m, conjs.size(), conjs.c_ptr());
+        return result;
     }
 
+    expr_ref to_formula(tbv const& t, doc_manager& m2, bool const* to_delete) {
+        expr_ref result(m);
+        expr_ref_vector conjs(m);
+        unsigned n = m2.num_tbits();
+        tbv_manager& tm = m2.tbvm();
+        for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
+            if (!to_delete[i]) {
+                switch (t[j]) {
+                case BIT_x:
+                    break;
+                case BIT_1:
+                    conjs.push_back(m_vars[i].get());
+                    break;
+                case BIT_0:
+                    conjs.push_back(m.mk_not(m_vars[i].get()));
+                    break;
+                default:
+                    UNREACHABLE();
+                    break;
+                }
+                ++j;
+            }
+        }
+        result = mk_and(m, conjs.size(), conjs.c_ptr());
+        return result;
+    }
+
+    expr_ref to_formula(doc const& d, doc_manager& m2, bool const* to_delete) {
+        expr_ref result(m);
+        expr_ref_vector conjs(m);
+        conjs.push_back(to_formula(d.pos(), m2, to_delete));
+        for (unsigned i = 0; i < d.neg().size(); ++i) {
+            conjs.push_back(m.mk_not(to_formula(d.neg()[i], m2, to_delete)));
+        }
+        result = mk_and(m, conjs.size(), conjs.c_ptr());
+        return result;
+    }
+
+    void project(doc const& d, doc_manager& m2, bool const* to_delete, doc_ref& result) {
+        result = dm.project(m2, m_vars.size(), to_delete, d);
+        TRACE("doc",
+              for (unsigned i = 0; i < m_vars.size(); ++i) {
+                  tout << (to_delete[i]?"0":"1");
+              }
+              tout << " ";
+              dm.display(tout, d) << " -> ";
+              m2.display(tout, *result) << "\n";
+              );        
+    } 
+
     void test_clauses(unsigned num_clauses) {
         doc_ref d(dm, dm.allocateX());
         expr_ref_vector fmls(m);
-        expr_ref fml(m);
+        th_rewriter rw(m);
+        expr_ref fml1(m), fml2(m), fml3(m), tmp1(m), tmp2(m), fml(m);
         for (unsigned i = 0; i < num_clauses; ++i) {
-            expr_ref clause(m);
             tbv* t = dm.tbvm().allocate();
-            mk_clause(clause, *t);
+            fmls.push_back(m.mk_not(mk_conj(*t)));
             d->neg().push_back(t);
-            fmls.push_back(clause);
         }
-        fml = mk_and(m, fmls.size(), fmls.c_ptr());
-        dm.display(std::cout, *d) << "\n";
-        std::cout << fml << "\n";
-        for (unsigned i = 0; i < m_vars.size(); ++i) {
-            //test_project(i, fml, *d);
-        }
-    }
-
-    void test_project(unsigned i, expr* fml, doc& d) {
+        fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
         svector<bool> to_delete(m_vars.size(), false);
-        to_delete[i] = true;
-        doc_manager dm1(m_vars.size()-1);
-        doc_ref d1(dm1, dm1.project(m_vars.size(), to_delete.c_ptr(), d));
-        expr_ref fml1(m);
-        // fml1 = m.mk_exists();
-        // extrac formula fml2 from d1,
-        // check that fml1 is equivalent to fml2
+        unsigned num_bits = 1;
+        for (unsigned i = 1; i < to_delete.size(); ++i) {
+            to_delete[i] = (m_ran(2) == 0);
+            if (!to_delete[i]) ++num_bits;
+        }
+        doc_manager m2(num_bits);
+        doc_ref result(m2);
+        project(*d, m2, to_delete.c_ptr(), result);
+        fml2 = to_formula(*result, m2, to_delete.c_ptr());
+        rw(fml2);
+        
+        for (unsigned i = 0; i < m_vars.size(); ++i) {
+            if (to_delete[i]) {
+                expr_safe_replace rep1(m), rep2(m);
+                rep1.insert(m_vars[i].get(), m.mk_true());
+                rep1(fml1, tmp1);
+                rep2.insert(m_vars[i].get(), m.mk_false());
+                rep2(fml1, tmp2);
+                fml1 = m.mk_or(tmp1, tmp2);
+            }
+        }
+        rw(fml1);
+        smt_params fp;
+        smt::kernel solver(m, fp);
+        TRACE("doc", tout << "manual project:\n" << fml1 << "\nautomatic project: \n" << fml2 << "\n";);
+        fml = m.mk_not(m.mk_eq(fml1, fml2));
+        solver.assert_expr(fml);
+        lbool res = solver.check();
+        SASSERT(res == l_false);
     }
 
 public:    
@@ -171,5 +243,5 @@ void tst_doc() {
     tst_doc1(70);
 
     test_doc_project tp(4);    
-    tp(5,7);
+    tp(200,7);
 }
diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp
index 21ecdd697..d56fcd84a 100644
--- a/src/test/tbv.cpp
+++ b/src/test/tbv.cpp
@@ -24,6 +24,16 @@ static void tst1(unsigned num_bits) {
     VERIFY(m.intersect(*bX,*b0,*bN));
     SASSERT(m.equals(*b0, *bN));
     VERIFY(!m.intersect(*b0,*b1,*bN));
+    m.fill1(*b1);
+    svector<bool> to_delete(num_bits, false);
+    tbv_manager m2(num_bits-2);
+    to_delete[1] = true;
+    to_delete[3] = true;
+    (*b1).set(2, BIT_0);
+    (*b1).set(4, BIT_x);
+    tbv_ref b2(m2, m2.project(num_bits, to_delete.c_ptr(), *b1));
+    m.display(std::cout, *b1) << " -> ";
+    m2.display(std::cout, *b2) << "\n";
     m.deallocate(b0);
     m.deallocate(b1);
     m.deallocate(bX);