diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 03f69bf5f..c8cef5c95 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -280,7 +280,7 @@ bool doc_manager::intersect(doc const& A, doc const& B, doc& result) {
 //   indices where BIT_0 is set are positive.
 //
 
-doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) {
+doc* doc_manager::project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src) {
     tbv_manager& dstt = dstm.m;    
     tbv_ref t(dstt);
     t = dstt.project(n, to_delete, src.pos());
@@ -391,7 +391,7 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
 
 doc_manager::project_action_t 
 doc_manager::pick_resolvent(
-    tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx) {
+    tbv const& pos, tbv_vector const& neg, bit_vector 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;   
@@ -401,7 +401,7 @@ doc_manager::pick_resolvent(
     unsigned best_neg = UINT_MAX;
     unsigned best_idx = UINT_MAX;
     for (unsigned i = 0; i < num_tbits(); ++i) {
-        if (!to_delete[i]) continue;
+        if (!to_delete.get(i)) continue;
         if (pos[i] != BIT_x) continue;
         unsigned num_pos = 0, num_neg = 0;
         tbit b1 = (*neg[0])[i];
@@ -480,7 +480,6 @@ void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
     for (unsigned i = 0; i < B.neg().size(); ++i) {
         r = allocate(A);
         if (set_and(*r, B.neg()[i])) {
-            r->neg().intersect(m, r->pos());
             result.push_back(r.detach());
         }
     }
@@ -566,7 +565,7 @@ std::ostream& doc_manager::display(std::ostream& out, doc const& b, unsigned hi,
 }
 
 
-void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst) {
+void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst) {
     expr_ref fml1 = to_formula(m, src);
     expr_ref fml2 = dstm.to_formula(m, dst);
     project_rename(fml2, to_delete);
@@ -603,11 +602,11 @@ expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
     return result;
 }
     
-void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
+void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) {
     ast_manager& m = fml.get_manager();
     expr_ref tmp1(m), tmp2(m);
     for (unsigned i = 0; i < num_tbits(); ++i) {
-        if (to_delete[i]) {
+        if (to_delete.get(i)) {
             expr_safe_replace rep1(m), rep2(m);
             rep1.insert(tbvm().mk_var(m, i), m.mk_true());
             rep1(fml, tmp1);
@@ -623,11 +622,11 @@ void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
     }
 }
 
-void doc_manager::project_rename(expr_ref& fml, bool const* to_delete) {
+void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) {
     ast_manager& m = fml.get_manager();
     expr_safe_replace rep(m);
     for (unsigned i = 0, j = 0; i < num_tbits(); ++i) {
-        if (!to_delete[i]) {
+        if (!to_delete.get(i)) {
             rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i));
             ++j;
         }
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index eccdd75b0..145f8d456 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -48,7 +48,7 @@ class doc_manager {
         project_resolve        
     };
     project_action_t pick_resolvent(
-        tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx);
+        tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx);
 public:
     doc_manager(unsigned num_bits);
     ~doc_manager();
@@ -88,17 +88,17 @@ public:
     std::ostream& display(std::ostream& out, doc const& b) const;
     std::ostream& display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const;
     unsigned num_tbits() const { return m.num_tbits(); }
-    doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src);
+    doc* project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src);
     bool well_formed(doc const& d) const;
     bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
     void set(doc& d, unsigned idx, tbit value);
 
-    void verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst);
+    void verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst);
 private:
     unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
     bool merge(doc& d, unsigned idx, subset_ints const& equalities, bit_vector const& discard_cols);
-    void project_rename(expr_ref& fml, bool const* to_delete);
-    void project_expand(expr_ref& fml, bool const* to_delete);
+    void project_rename(expr_ref& fml, bit_vector const& to_delete);
+    void project_expand(expr_ref& fml, bit_vector const& to_delete);
     expr_ref to_formula(ast_manager& m, doc const& src);
     void check_equiv(ast_manager& m, expr* fml1, expr* fml2);
 };
@@ -171,11 +171,13 @@ public:
         SASSERT(t);
         unsigned sz = size(), j = 0;
         bool found = false;
-        for (unsigned i = 0; i < sz; ++i, ++j) {
+        unsigned i = 0;
+        for ( ; i < sz; ++i, ++j) {
             if (m.contains(*m_elems[i], *t)) {
                 found = true;
+                break;
             }
-            if (!found && m.contains(*t, *m_elems[i])) {
+            if (m.contains(*t, *m_elems[i])) {
                 m.deallocate(m_elems[i]);
                 --j;
             }
@@ -185,6 +187,7 @@ public:
         }
         if (j != sz) m_elems.resize(j);
         if (found) {
+            SASSERT(j == i);
             m.deallocate(t);
         }
         else {
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 4ea8f48f6..8e213fadc 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -99,11 +99,11 @@ tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
     }
     return r;
 }
-tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
+tbv* tbv_manager::project(unsigned n, bit_vector const& to_delete, tbv const& src) {
     tbv* r = allocate();
     unsigned i, j;
     for (i = 0, j = 0; i < n; ++i) {
-        if (!to_delete[i]) {
+        if (!to_delete.get(i)) {
             set(*r, j, src[i]);
             ++j;
         }
diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
index 9663f7d04..39067c64c 100644
--- a/src/muz/rel/tbv.h
+++ b/src/muz/rel/tbv.h
@@ -76,7 +76,7 @@ public:
     bool intersect(tbv const& a, tbv const& b, tbv& result);
     std::ostream& display(std::ostream& out, tbv const& b) const;
     std::ostream& display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const;
-    tbv* project(unsigned n, bool const* to_delete, tbv const& src);
+    tbv* project(unsigned n, bit_vector const& to_delete, tbv const& src);
     bool is_well_formed(tbv const& b) const; // - does not contain BIT_z;
     void set(tbv& dst, uint64 n, unsigned hi, unsigned lo);
     void set(tbv& dst, rational const& r, unsigned hi, unsigned lo);
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 4e46a463f..459b94101 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -54,9 +54,6 @@ Notes:
      return tgt \ join_project(tgt, neg, c1, .., cN, d1, .. , dN)
      We have most of the facilities required for a join project operation.
      For example, the filter_project function uses both equalities and deleted columns.
-   - Lipstick service:
-     - filter_proj_fn uses both a bit_vector and a svector<bool> for representing removed bits. 
-       This is due to underlying routines using different types for the same purpose. 
 --*/
 #include "udoc_relation.h"
 #include "dl_relation_manager.h"
@@ -473,7 +470,7 @@ namespace datalog {
     }
 
     class udoc_plugin::project_fn : public convenient_relation_project_fn {
-        svector<bool> m_to_delete;
+        bit_vector m_to_delete;
     public:
         project_fn(udoc_relation const & t, unsigned removed_col_cnt, const unsigned * removed_cols) 
             : convenient_relation_project_fn(t.get_signature(), removed_col_cnt, removed_cols) {
@@ -481,7 +478,7 @@ namespace datalog {
             unsigned n = t.get_dm().num_tbits();
             m_to_delete.resize(n, false);
             for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
-                m_to_delete[m_removed_cols[i]] = true;
+                m_to_delete.set(m_removed_cols[i], true);
             }
         }
 
@@ -496,7 +493,7 @@ namespace datalog {
             udoc const& ud1 = t.get_udoc();
             udoc& ud2 = r->get_udoc();
             for (unsigned i = 0; i < ud1.size(); ++i) {
-                d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), ud1[i]);
+                d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete, ud1[i]);
                 ud2.push_back(d2.detach());
             }
             TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';);
@@ -1198,8 +1195,7 @@ namespace datalog {
         expr_ref     m_reduced_condition;
         udoc         m_udoc;
         udoc         m_udoc2;
-        bit_vector   m_col_list; // map: col idx -> bool (whether the column is to be removed)
-        svector<bool> m_to_delete; // same
+        bit_vector   m_to_delete; // map: col idx -> bool (whether the column is to be removed)
         subset_ints  m_equalities;
         unsigned_vector m_roots;
 
@@ -1213,19 +1209,17 @@ namespace datalog {
             m_equalities(union_ctx) {
             unsigned num_bits = t.get_num_bits();
             t.expand_column_vector(m_removed_cols);
-            m_col_list.resize(num_bits,  false);
             m_to_delete.resize(num_bits, false);
             for (unsigned i = 0; i < num_bits; ++i) {
                 m_equalities.mk_var();
             }        
             for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
-                m_col_list.set(m_removed_cols[i], true);
-                m_to_delete[m_removed_cols[i]] = true;
+                m_to_delete.set(m_removed_cols[i], true);
             }
             expr_ref guard(m), non_eq_cond(condition, m);
             t.extract_equalities(condition, non_eq_cond, m_equalities, m_roots);
             t.extract_guard(non_eq_cond, guard, m_reduced_condition);            
-            t.compile_guard(guard, m_udoc, m_col_list);
+            t.compile_guard(guard, m_udoc, m_to_delete);
         }
         
         virtual ~filter_proj_fn() {
@@ -1238,13 +1232,13 @@ namespace datalog {
             ast_manager& m = m_reduced_condition.get_manager();
             m_udoc2.copy(dm, u1);
             m_udoc2.intersect(dm, m_udoc);
-            t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_col_list);
-            m_udoc2.merge(dm, m_roots, m_equalities, m_col_list);
+            t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_to_delete);
+            m_udoc2.merge(dm, m_roots, m_equalities, m_to_delete);
             SASSERT(m_udoc2.well_formed(dm));  
             udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
             doc_manager& dm2 = r->get_dm();
             for (unsigned i = 0; i < m_udoc2.size(); ++i) {
-                doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), m_udoc2[i]);
+                doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete, m_udoc2[i]);
                 r->get_udoc().insert(dm2, d);
                 SASSERT(r->get_udoc().well_formed(dm2));
             }