diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 36717adf3..4018441a1 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -82,12 +82,8 @@ void doc_manager::deallocate(doc* src) {
 }
 void doc_manager::copy(doc& dst, doc const& src)  {
     m.copy(dst.pos(), src.pos());
-    unsigned n = std::min(src.neg().size(), dst.neg().size());
-    for (unsigned i = 0; i < n; ++i) {
-        m.copy(dst.neg()[i], src.neg()[i]);
-    }
     dst.neg().reset(m);
-    for (unsigned i = n; i < src.neg().size(); ++i) {
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
         dst.neg().push_back(m.allocate(src.neg()[i]));
     }
 }
@@ -109,16 +105,17 @@ 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;
-    dst.neg().intersect(m, dst.pos());
+    dst.neg().intersect(m, dst.pos());    
     tbv_ref t(m);
     for (unsigned i = 0; i < src.neg().size(); ++i) {
         t = m.allocate(src.neg()[i]);
         if (m.set_and(*t, dst.pos())) {
+            if (m.equals(*t, dst.pos())) return false;
             dst.neg().insert(m, t.detach());
         }
     }
     SASSERT(well_formed(dst));
-    return (src.neg().is_empty() || fold_neg(dst));
+    return fold_neg(dst);
 }
 bool doc_manager::set_and(doc& dst, tbv const& src)  {
     // (A \ B) & C  = (A & C) \ B
@@ -279,80 +276,60 @@ bool doc_manager::intersect(doc const& A, doc const& B, doc& result) {
 //
 
 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()));
+    tbv_manager& dstt = dstm.m;    
+    tbv_ref t(dstt);
+    t = dstt.project(n, to_delete, src.pos());
+    doc* r = dstm.allocate(t.detach());
     SASSERT(r);
 
     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;
-    }
-    
-    //
-    // 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;
+    tbv_vector todo, new_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]));
-        }
+        todo.push_back(tbvm().allocate(src.neg()[i]));
     }
-    if (todo.empty()) {
-        return r;
-    }
-    ptr_vector<tbv> new_todo;
-    utbv pos, neg;
-    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";);
-            SASSERT(pos.is_empty());
-            SASSERT(neg.is_empty());
-            SASSERT(new_todo.empty());
-            while (!todo.empty()) {
-                tbv* t = todo.back();
-                todo.pop_back();
-                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;                    
+    unsigned idx;
+    bool done = false;
+    while (!todo.empty() && !done) {
+        switch(pick_resolvent(src.pos(), todo, to_delete, idx)) {
+        case project_is_empty: 
+            t = dstt.allocate(r->pos());
+            r->neg().push_back(t.detach());
+            done = true;
+            break;
+        case project_monolithic:
+            done = true;
+            break;
+        case project_neg:
+        case project_pos:
+            for (unsigned i = 0; i < todo.size(); ++i) {
+                tbv& tx = *todo[i];
+                if (tx[idx] == BIT_x) {
+                    new_todo.push_back(&tx);
+                }
+                else {
+                    m.deallocate(&tx);
                 }
             }
-            if (pos.is_empty() || neg.is_empty()) {
-                std::swap(new_todo, todo);
-                pos.reset(tbvm());
-                neg.reset(tbvm());
-                continue;
+            std::swap(new_todo, todo);
+            new_todo.reset();
+            break;        
+        case project_resolve: {
+            utbv pos, neg;
+            for (unsigned i = 0; i < todo.size(); ++i) {
+                tbv& tx = *todo[i];
+                switch(tx[idx]) {
+                case BIT_x: new_todo.push_back(&tx); break;
+                case BIT_0: neg.push_back(&tx); break;
+                case BIT_1: pos.push_back(&tx); break;
+                default: UNREACHABLE(); break;                    
+                }
             }
             TRACE("doc",
                   tout << "pos: ";
@@ -365,38 +342,120 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
                   }
                   tout << "\n";
                   );
-                  
+            SASSERT(pos.size() > 0 && neg.size() > 0);
+            tbv_ref t1(m);
             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);
+                    t1 = m.allocate(pos[j]);
+                    (*t1).set(idx, BIT_x);
                     if (tbvm().set_and(*t1, neg[k])) {
-                        (*t1).set(i, BIT_x);
+                        (*t1).set(idx, BIT_x);
                         new_todo.push_back(t1.detach());
                     }
-                }                
-            }
-            pos.reset(tbvm());
-            neg.reset(tbvm());
+                }       
+            }         
+            pos.reset(m);
+            neg.reset(m);
             std::swap(todo, new_todo);
+            new_todo.reset();
+            break;
+        }
+        case project_done: {
+            for (unsigned i = 0; i < todo.size(); ++i) {
+                t = dstt.project(n, to_delete, *todo[i]);
+                if (dstt.equals(r->pos(), *t)) {
+                    r->neg().reset(dstt);
+                    r->neg().push_back(t.detach());
+                    break;
+                }
+                if (r->neg().size() > 0 && dstt.equals(r->neg()[0], *t)) {
+                    continue;
+                }
+                r->neg().push_back(t.detach());
+            }
+            done = true;
+            break;
+        }
         }
     }
     for (unsigned i = 0; i < todo.size(); ++i) {
-        r->neg().push_back(dstt.project(n, to_delete, *todo[i]));
-        tbvm().deallocate(todo[i]);
+        m.deallocate(todo[i]);
     }
     return r;
 }
 
+#if 0
 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;
 }
+#endif
+
+doc_manager::project_action_t 
+doc_manager::pick_resolvent(
+    tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx) {
+    if (neg.empty()) return project_done;
+    for (unsigned j = 0; j < neg.size(); ++j) {
+        if (m.equals(pos, *neg[j])) return project_is_empty;   
+    } 
+
+    unsigned best_pos = UINT_MAX;
+    unsigned best_neg = UINT_MAX;
+    unsigned best_idx = UINT_MAX;
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        if (!to_delete[i]) continue;
+        if (pos[i] != BIT_x) continue;
+        unsigned num_pos = 0, num_neg = 0;
+        tbit b1 = (*neg[0])[i];
+        if (b1 == BIT_0) num_neg++; 
+        if (b1 == BIT_1) num_pos++;
+        bool monolithic = true;
+        for (unsigned j = 1; j < neg.size(); ++j) {
+            tbit b2 = (*neg[j])[i];
+            if (b1 != b2) {
+                monolithic = false;
+            }
+            if (b2 == BIT_0) num_neg++; 
+            if (b2 == BIT_1) num_pos++;
+        }
+        if (monolithic && b1 != BIT_x) {
+            idx = i;
+            return project_monolithic;
+        }
+        if (monolithic && b1 == BIT_x) {
+            continue;
+        }
+        SASSERT(!monolithic);
+        if (num_pos == 0) {
+            SASSERT(num_neg > 0);
+            idx = i;
+            return project_neg;
+        }
+        if (num_neg == 0) {
+            SASSERT(num_pos > 0);
+            idx = i;
+            return project_pos;
+        }
+        if ((best_pos >= num_pos && best_neg >= num_neg) ||
+            num_neg == 1 || num_pos == 1) {
+            best_pos = num_pos;
+            best_neg = num_neg;
+            best_idx = i;
+        }
+    }
+    if (best_idx != UINT_MAX) {
+        idx = best_idx;
+        return project_resolve;
+    }
+    else {
+        return project_done;
+    }
+}
     
 
-void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
+void doc_manager::complement(doc const& src, doc_vector& result) {
     result.reset();
     if (is_full(src)) {
         return;
@@ -411,7 +470,7 @@ void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
 // (A \ {A1}) \ (B \ {B1})
 // (A & !A1 & & !B) |  (A & B1 & !A1)
 // A \ {A1 u B} u (A & B1) \ {A1}
-void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result) {
+void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
     doc_ref r(*this);
     tbv_ref t(m);
     r = allocate(A);
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index 58850f812..30858bbbd 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -25,16 +25,30 @@ Revision History:
 
 #include "tbv.h"
 #include "union_find.h"
+#include "buffer.h"
 
 
 class doc;
 template<typename M, typename T> class union_bvec;
 typedef union_find<> subset_ints;
+typedef union_bvec<tbv_manager, tbv> utbv;
+typedef buffer<tbv*,false,8> tbv_vector;
+typedef buffer<doc*,false,8> doc_vector;
 
 class doc_manager {
     tbv_manager m;
     tbv*        m_full;
     small_object_allocator m_alloc;
+    enum project_action_t {
+        project_is_empty,
+        project_done,
+        project_monolithic,
+        project_neg,
+        project_pos,
+        project_resolve        
+    };
+    project_action_t pick_resolvent(
+        tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx);
 public:
     doc_manager(unsigned num_bits);
     ~doc_manager();
@@ -62,8 +76,8 @@ public:
     bool set_and(doc& dst, tbv const& src);
     bool fold_neg(doc& dst);
     bool intersect(doc const& A, doc const& B, doc& result);
-    void complement(doc const& src, ptr_vector<doc>& result);
-    void subtract(doc const& A, doc const& B, ptr_vector<doc>& result);
+    void complement(doc const& src, doc_vector& result);
+    void subtract(doc const& A, doc const& B, doc_vector& result);
     bool equals(doc const& a, doc const& b) const;
     unsigned hash(doc const& src) const;
     bool contains(doc const& a, doc const& b) const;
@@ -83,7 +97,7 @@ private:
 // union of tbv*, union of doc*
 template<typename M, typename T>
 class union_bvec { 
-    ptr_vector<T> m_elems; // TBD: reuse allocator of M
+    buffer<T*, false, 8> m_elems; // TBD: reuse allocator of M
 
     enum fix_bit_result_t {
         e_row_removed, // = 1
@@ -278,7 +292,6 @@ public:
 
 };
 
-typedef union_bvec<tbv_manager, tbv> utbv;
 
 class doc {
     // pos \ (neg_0 \/ ... \/ neg_n)
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 0dcbcade9..6f175f8de 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -130,9 +130,7 @@ void tbv::set(rational const& r, unsigned hi, unsigned lo) {
 }
 
 void tbv::set(tbv const& other, unsigned hi, unsigned lo) {
-    for (unsigned i = 0; i < hi - lo + 1; ++i) {
-        set(lo + i, other[i]);
-    }
+    fixed_bit_vector::set(other, 2*hi+1, 2*lo);
 }
 
 
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index f4b758c5e..110c75ef4 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -743,7 +743,7 @@ namespace datalog {
         }        
         apply_guard(g, result, equalities, discard_cols);
     }
-    bool udoc_relation::apply_eq(expr* g, udoc& result, unsigned v, unsigned hi, unsigned lo, expr* c) const {
+    bool udoc_relation::apply_eq(expr* g, doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const {
         udoc_plugin& p = get_plugin();
         unsigned num_bits;
         rational r;
@@ -751,9 +751,8 @@ namespace datalog {
         lo += col;
         hi += col;
         if (p.is_numeral(c, r, num_bits)) {
-            doc_ref d(dm, dm.allocateX());
+            d = dm.allocateX();
             d->pos().set(r, hi, lo);
-            result.intersect(dm, *d);
             return true;
         }
         // other cases?
@@ -764,7 +763,9 @@ namespace datalog {
         expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const {
         ast_manager& m = get_plugin().get_ast_manager();
         bv_util& bv = get_plugin().bv;
-        expr* e1, *e2;
+        expr *e0, *e1, *e2;
+        unsigned hi, lo, lo1, lo2, hi1, hi2, v, v1, v2;
+        doc_ref d(get_dm());
         if (result.is_empty()) {
         }
         else if (m.is_true(g)) {
@@ -777,6 +778,18 @@ namespace datalog {
                 apply_guard(to_app(g)->get_arg(i), result, equalities, discard_cols);
             }
         }
+        else if (m.is_not(g, e0) &&
+                 m.is_eq(e0, e1, e2) && bv.is_bv(e1) &&
+                 is_var_range(e1, hi, lo, v) && is_ground(e2) &&
+                 apply_eq(g, d, v, hi, lo, e2)) {
+            result.subtract(dm, *d);
+        }
+        else if (m.is_not(g, e0) &&
+                 m.is_eq(e0, e2, e1) && bv.is_bv(e1) &&
+                 is_var_range(e1, hi, lo, v) && is_ground(e2) &&
+                 apply_eq(g, d, v, hi, lo, e2)) {
+            result.subtract(dm, *d);
+        }
         else if (m.is_not(g, e1)) {
             udoc sub;
             sub.push_back(dm.allocateX());
@@ -830,12 +843,13 @@ namespace datalog {
             diff2.reset(dm);
         }
         else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
-            unsigned hi, lo, lo1, lo2, hi1, hi2, v, v1, v2;
             if (is_var_range(e1, hi, lo, v) && is_ground(e2) &&
-                apply_eq(g, result, v, hi, lo, e2)) {
+                apply_eq(g, d, v, hi, lo, e2)) {
+                result.intersect(dm, *d);
             }
             else if (is_var_range(e2, hi, lo, v) && is_ground(e1) &&
-                     apply_eq(g, result, v, hi, lo, e1)) {
+                     apply_eq(g, d, v, hi, lo, e1)) {
+                result.intersect(dm, *d);
             }
             else if (is_var_range(e1, hi1, lo1, v1) && 
                      is_var_range(e2, hi2, lo2, v2)) {
diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h
index c3ce8d2c4..1d14062e6 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/src/muz/rel/udoc_relation.h
@@ -70,7 +70,7 @@ namespace datalog {
         void extract_equalities(expr* g, expr_ref& rest, subset_ints& equalities, unsigned_vector& roots) const;
         void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
         void apply_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const;
-        bool apply_eq(expr* g, udoc& result, unsigned v, unsigned hi, unsigned lo, expr* c) const;
+        bool apply_eq(expr* g, doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const;
         bool is_var_range(expr* e, unsigned& hi, unsigned& lo, unsigned& v) const;
     };
 
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index 45206d4ca..409debfb0 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -170,49 +170,47 @@ class test_doc_cls {
         return result;
     }
 
-    expr_ref to_formula(tbv const& t, doc_manager& m2, bool const* to_delete) {
+    expr_ref to_formula(tbv const& t, doc_manager& m2) {
         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;
+        SASSERT(n <= m_vars.size());
+        for (unsigned i = 0; i < n; ++i) {
+            switch (t[i]) {
+            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;
             }
         }
         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 to_formula(doc const& d, doc_manager& m2) {
         expr_ref result(m);
         expr_ref_vector conjs(m);
-        conjs.push_back(to_formula(d.pos(), m2, to_delete));
+        conjs.push_back(to_formula(d.pos(), m2));
         for (unsigned i = 0; i < d.neg().size(); ++i) {
-            conjs.push_back(m.mk_not(to_formula(d.neg()[i], m2, to_delete)));
+            conjs.push_back(m.mk_not(to_formula(d.neg()[i], m2)));
         }
         result = mk_and(m, conjs.size(), conjs.c_ptr());
         return result;
     }
 
-    expr_ref to_formula(udoc const& ud, doc_manager& m2, bool const* to_delete) {
+    expr_ref to_formula(udoc const& ud, doc_manager& m2) {
         expr_ref result(m);
         expr_ref_vector disjs(m);
         for (unsigned i = 0; i < ud.size(); ++i) {
-            disjs.push_back(to_formula(ud[i], m2, to_delete));
+            disjs.push_back(to_formula(ud[i], m2));
         }
         result = mk_or(m, disjs.size(), disjs.c_ptr());
         return result;
@@ -230,17 +228,12 @@ class test_doc_cls {
               );        
     } 
 
+
     void test_project(unsigned num_clauses) {
-        doc_ref d(dm, dm.allocateX());
-        expr_ref_vector fmls(m);
-        th_rewriter rw(m);
+        doc_ref d(dm);
+        d = mk_rand_doc(3);
         expr_ref fml1(m), fml2(m), fml3(m), tmp1(m), tmp2(m), fml(m);
-        for (unsigned i = 0; i < num_clauses; ++i) {
-            tbv* t = dm.tbvm().allocate();
-            fmls.push_back(m.mk_not(mk_conj(*t)));
-            d->neg().push_back(t);
-        }
-        fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
+        fml1 = to_formula(*d, dm);
         svector<bool> to_delete(m_vars.size(), false);
         unsigned num_bits = 1;
         for (unsigned i = 1; i < to_delete.size(); ++i) {
@@ -250,33 +243,43 @@ class test_doc_cls {
         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);
-        
+        TRACE("doc",              
+              dm.display(tout, *d) << "\n";
+              m2.display(tout, *result) << "\n";);
+        fml2 = to_formula(*result, m2);
+        project_expand(fml1, to_delete.c_ptr());
+        project_rename(fml2, to_delete.c_ptr());
+        check_equiv(fml1, fml2);
+    }
+
+    void project_expand(expr_ref& fml, bool const* to_delete) {
+        expr_ref tmp1(m), tmp2(m);
         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);
+                rep1(fml, tmp1);
                 rep2.insert(m_vars[i].get(), m.mk_false());
-                rep2(fml1, tmp2);
-                fml1 = m.mk_or(tmp1, tmp2);
+                rep2(fml, tmp2);
+                fml = 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);
+    }
+
+    void project_rename(expr_ref& fml, bool const* to_delete) {
+        expr_safe_replace rep(m);
+        for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
+            if (!to_delete[i]) {
+                rep.insert(m_vars[j].get(), m_vars[i].get());
+                ++j;
+            }
+        }
+        rep(fml);
     }
 
     void test_merge(unsigned num_clauses) {
         doc_ref d(dm, dm.allocateX());
         expr_ref_vector fmls(m), eqs(m);
-        th_rewriter rw(m);
         unsigned N = m_vars.size();
         expr_ref fml1(m), fml2(m), fml3(m), tmp1(m), tmp2(m), fml(m);
         for (unsigned i = 0; i < num_clauses; ++i) {
@@ -305,20 +308,21 @@ class test_doc_cls {
                 eqs.push_back(m.mk_eq(m_vars[i].get(), m_vars[lo].get()));
             }
         }
-        eqs.push_back(to_formula(*d, dm, to_delete.c_ptr()));
+        eqs.push_back(to_formula(*d, dm));
         fml1 = mk_and(m, eqs.size(), eqs.c_ptr());
         if (dm.merge(*d, lo, 1, equalities, discard_cols)) {
-            fml2 = to_formula(*d, dm, to_delete.c_ptr());
+            fml2 = to_formula(*d, dm);
         }
         else {
             fml2 = m.mk_false();
         }
-        rw(fml1);
-        rw(fml2);
         check_equiv(fml1, fml2);
     }
 
-    void check_equiv(expr* fml1, expr* fml2) {
+    void check_equiv(expr_ref& fml1, expr_ref& fml2) {
+        th_rewriter rw(m);
+        rw(fml1);
+        rw(fml2);
         smt_params fp;
         smt::kernel solver(m, fp);
         expr_ref fml(m);
@@ -355,6 +359,29 @@ public:
         }    
     }
 
+    void test_project1() {
+        expr_ref fml1(m), fml2(m);
+        doc_ref d(dm, dm.allocateX());
+        tbv_ref t(dm.tbvm(), dm.tbvm().allocateX());
+        t->set(0, BIT_0);
+        d->neg().push_back(t.detach());
+        unsigned num_bits = dm.num_tbits();
+        svector<bool> to_delete(num_bits, false);
+        fml1 = to_formula(*d, dm);
+        to_delete[0] = true;
+        doc_manager m2(num_bits-1);
+        doc_ref result(m2);
+        project(*d, m2, to_delete.c_ptr(), result);
+        dm.display(std::cout, *d) << "\n";
+        m2.display(std::cout, *result) << "\n";
+        fml2 = to_formula(*result, m2);
+        project_rename(fml2, to_delete.c_ptr());
+        project_expand(fml1, to_delete.c_ptr());
+        std::cout << fml1 << " " << fml2 << "\n";
+        check_equiv(fml1, fml2);
+    }
+
+
     void test_subtract() {
         doc_ref d1(dm);
         doc_ref d2(dm);
@@ -384,12 +411,11 @@ public:
         ds2.push_back(d1.detach());
         ds1.display(dm, std::cout) << "\n";
         ds2.display(dm, std::cout) << "\n";
-        svector<bool> to_delete(m_vars.size(), false);
-        expr_ref fml1 = to_formula(ds1, dm, to_delete.c_ptr());
-        expr_ref fml2 = to_formula(ds2, dm, to_delete.c_ptr());
+        expr_ref fml1 = to_formula(ds1, dm);
+        expr_ref fml2 = to_formula(ds2, dm);
         ds1.subtract(dm, ds2);
         ds1.display(dm, std::cout) << "\n";
-        expr_ref fml3 = to_formula(ds1, dm, to_delete.c_ptr());
+        expr_ref fml3 = to_formula(ds1, dm);
         fml1 = m.mk_and(fml1, m.mk_not(fml2));
         check_equiv(fml1, fml3);       
         ds1.reset(dm);
@@ -401,10 +427,10 @@ public:
             udoc d1, d2;
             mk_rand_udoc(3, 3, d1);
             mk_rand_udoc(3, 3, d2);
-            fml1 = to_formula(d1, dm, to_delete.c_ptr());
-            fml2 = to_formula(d2, dm, to_delete.c_ptr());
+            fml1 = to_formula(d1, dm);
+            fml2 = to_formula(d2, dm);
             d1.subtract(dm, d2);
-            fml3 = to_formula(d1, dm, to_delete.c_ptr());
+            fml3 = to_formula(d1, dm);
             fml1 = m.mk_and(fml1, m.mk_not(fml2));
             check_equiv(fml1, fml3);
             d1.reset(dm);
@@ -414,20 +440,19 @@ public:
 
     void test_intersect() {
         expr_ref fml1(m), fml2(m), fml3(m);
-        svector<bool> to_delete(m_vars.size(), false);
         for (unsigned i = 0; i < 10000; ++i) {
             udoc d1, d2;
             mk_rand_udoc(3, 3, d1);
             mk_rand_udoc(3, 3, d2);
-            fml1 = to_formula(d1, dm, to_delete.c_ptr());
-            fml2 = to_formula(d2, dm, to_delete.c_ptr());
+            fml1 = to_formula(d1, dm);
+            fml2 = to_formula(d2, dm);
             TRACE("doc", 
                   d1.display(dm, tout) << "\n";
                   d2.display(dm, tout) << "\n";);
             d1.intersect(dm, d2);
             TRACE("doc", d1.display(dm, tout) << "\n";);
             SASSERT(d1.well_formed(dm));
-            fml3 = to_formula(d1, dm, to_delete.c_ptr());
+            fml3 = to_formula(d1, dm);
             fml1 = m.mk_and(fml1, fml2);
             check_equiv(fml1, fml3);
             d1.reset(dm);
@@ -441,10 +466,12 @@ public:
 void tst_doc() {
 
     test_doc_cls tp(4);
+    tp.test_project1();
+    tp.test_project(200,7);
+
     tp.test_intersect();
     tp.test_subtract();
     tp.test_merge(200,7);
-    tp.test_project(200,7);
 
     tst_doc1(5);
     tst_doc1(10);
diff --git a/src/util/fixed_bit_vector.cpp b/src/util/fixed_bit_vector.cpp
index 3711ef5eb..78196f568 100644
--- a/src/util/fixed_bit_vector.cpp
+++ b/src/util/fixed_bit_vector.cpp
@@ -24,6 +24,22 @@ Revision History:
 #include"trace.h"
 #include"hash.h"
 
+void fixed_bit_vector::set(fixed_bit_vector const& other, unsigned hi, unsigned lo) {
+    if ((lo % 32) == 0) {
+        unsigned sz32 = (hi+1)/32;
+        unsigned lo32 = lo/32;
+        for (unsigned i = 0; i < sz32; ++i) {
+            m_data[lo32 + i] = other.m_data[i];
+        }
+        for (unsigned i = sz32*32; i < hi - lo + 1; ++i) {
+            set(lo + i, other.get(i));
+        }
+        return;
+    }
+    for (unsigned i = 0; i < hi - lo + 1; ++i) {
+        set(lo + i, other.get(i));
+    }
+}
 
 fixed_bit_vector_manager::fixed_bit_vector_manager(unsigned num_bits):
     m_alloc("fixed_bit_vector") {
diff --git a/src/util/fixed_bit_vector.h b/src/util/fixed_bit_vector.h
index 4ada982d0..fb7ed38e9 100644
--- a/src/util/fixed_bit_vector.h
+++ b/src/util/fixed_bit_vector.h
@@ -72,6 +72,9 @@ public:
         get_bit_word(bit_idx) ^= (-_val ^ get_bit_word(bit_idx)) & get_pos_mask(bit_idx);
     }
 
+    // assign bits this[lo:hi] := other[0:hi-lo+1]
+    void set(fixed_bit_vector const& other, unsigned hi, unsigned lo);
+
 };
 
 class fixed_bit_vector_manager {