diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 4018441a1..bb9e0e649 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -147,7 +147,7 @@ bool doc_manager::fold_neg(doc& dst) {
                 --i;
             }
             else { // count == 1:
-                dst.pos().set(index, neg(dst.neg()[i][index]));
+                m.set(dst.pos(), index, neg(dst.neg()[i][index]));
                 dst.neg().intersect(tbvm(), dst.pos());
                 goto start_over;
             }
@@ -179,9 +179,9 @@ unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& inde
 }
 
 void doc_manager::set(doc& d, unsigned idx, tbit value) {
-    d.pos().set(idx, value);
+    m.set(d.pos(), idx, value);
     for (unsigned i = 0; i < d.neg().size(); ++i) {
-        d.neg()[i].set(idx, value);
+        m.set(d.neg()[i], idx, value);
     }
 }
 
@@ -243,13 +243,13 @@ bool doc_manager::merge(doc& d, unsigned idx, subset_ints const& equalities,
     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);
+                tbv* t = m.allocate(d.pos());
+                m.set(*t, idx, BIT_0);
+                m.set(*t, root1, BIT_1);
                 d.neg().insert(tbvm(), t);
-                t = tbvm().allocate(d.pos());
-                t->set(idx, BIT_1);
-                t->set(root1, BIT_0);
+                t = m.allocate(d.pos());
+                m.set(*t, idx, BIT_1);
+                m.set(*t, root1, BIT_0);
                 d.neg().insert(tbvm(), t);                
             }
             idx = equalities.next(idx);
@@ -347,9 +347,9 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
             for (unsigned j = 0; j < pos.size(); ++j) {
                 for (unsigned k = 0; k < neg.size(); ++k) {
                     t1 = m.allocate(pos[j]);
-                    (*t1).set(idx, BIT_x);
+                    m.set(*t1, idx, BIT_x);
                     if (tbvm().set_and(*t1, neg[k])) {
-                        (*t1).set(idx, BIT_x);
+                        m.set(*t1, idx, BIT_x);
                         new_todo.push_back(t1.detach());
                     }
                 }       
@@ -517,7 +517,7 @@ bool doc_manager::is_empty(doc const& src)  {
             tbit b2 = src.neg()[i][j];
             found = (b1 == BIT_x && b2 != BIT_x);
             if (found) {
-                pos->set(j, neg(b2));
+                m.set(*pos, j, neg(b2));
             }
         }
         if (!found) {
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 6f175f8de..23a96981d 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -76,9 +76,9 @@ tbv* tbv_manager::allocate(uint64 val) {
     for (unsigned bit = num_tbits(); bit > 0;) {
         --bit;
         if (val & (1ULL << bit)) {                        
-            v->set(bit, BIT_1);
+            set(*v, bit, BIT_1);
         } else {
-            v->set(bit, BIT_0);
+            set(*v, bit, BIT_0);
         }
     }
     return v;
@@ -87,14 +87,14 @@ tbv* tbv_manager::allocate(uint64 val) {
 tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) {
     tbv* v = allocateX();
     SASSERT(64 >= num_tbits() && num_tbits() > hi && hi >= lo);
-    v->set(val, hi, lo);
+    set(*v, val, hi, lo);
     return v;
 }
 tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
     tbv* r = allocate();
     unsigned sz = num_tbits();
     for (unsigned i = 0; i < sz; ++i) {
-        r->set(permutation[i], bv[i]);
+        set(*r, permutation[i], bv[i]);
     }
     return r;
 }
@@ -103,7 +103,7 @@ tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
     unsigned i, j;
     for (i = 0, j = 0; i < n; ++i) {
         if (!to_delete[i]) {
-            r->set(j, src[i]);
+            set(*r, j, src[i]);
             ++j;
         }
     }
@@ -111,26 +111,35 @@ tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
     return r;
 }
 
-void tbv::set(uint64 val, unsigned hi, unsigned lo) {
+void tbv_manager::set(tbv& dst, unsigned index, tbit value) {
+    SASSERT(index < num_tbits());
+    m.set(dst, 2*index,   (value & 2) != 0);
+    m.set(dst, 2*index+1, (value & 1) != 0);    
+}
+
+
+void tbv_manager::set(tbv& dst, uint64 val, unsigned hi, unsigned lo) {
+    SASSERT(lo <= hi && hi < num_tbits());
     for (unsigned i = 0; i < hi - lo + 1; ++i) {
-        set(lo + i, (val & (1ULL << i))?BIT_1:BIT_0);
+        set(dst, lo + i, (val & (1ULL << i))?BIT_1:BIT_0);
     }
 }
-void tbv::set(rational const& r, unsigned hi, unsigned lo) {
+void tbv_manager::set(tbv& dst, rational const& r, unsigned hi, unsigned lo) {
+    SASSERT(lo <= hi && hi < num_tbits());
     if (r.is_uint64()) {
-        set(r.get_uint64(), hi, lo);
+        set(dst, r.get_uint64(), hi, lo);
         return;
     }
     for (unsigned i = 0; i < hi - lo + 1; ++i) {
         if (bitwise_and(r, rational::power_of_two(i)).is_zero())
-            set(lo + i, BIT_0);
+            set(dst, lo + i, BIT_0);
         else
-            set(lo + i, BIT_1);
+            set(dst, lo + i, BIT_1);
     }
 }
 
-void tbv::set(tbv const& other, unsigned hi, unsigned lo) {
-    fixed_bit_vector::set(other, 2*hi+1, 2*lo);
+void tbv_manager::set(tbv& dst, tbv const& other, unsigned hi, unsigned lo) {
+    dst.set(other, 2*hi+1, 2*lo);
 }
 
 
@@ -142,9 +151,9 @@ tbv* tbv_manager::allocate(rational const& r) {
     for (unsigned bit = num_tbits(); bit > 0; ) {
         --bit;
         if (bitwise_and(r, rational::power_of_two(bit)).is_zero()) {
-            v->set(bit, BIT_0);
+            set(*v, bit, BIT_0);
         } else {
-            v->set(bit, BIT_1);
+            set(*v, bit, BIT_1);
         }
     }            
     return v;
@@ -211,12 +220,12 @@ void tbv_manager::complement(tbv const& src, ptr_vector<tbv>& result) {
         switch (src.get(i)) {
         case BIT_0:
             r = allocate(src);
-            r->set(i, BIT_1);
+            set(*r, i, BIT_1);
             result.push_back(r);
             break;
         case BIT_1:
             r = allocate(src);
-            r->set(i, BIT_0);
+            set(*r, i, BIT_0);
             result.push_back(r);
             break;
         default:
diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
index 90965f7d0..e701efcbe 100644
--- a/src/muz/rel/tbv.h
+++ b/src/muz/rel/tbv.h
@@ -73,6 +73,11 @@ public:
     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;
+    void set(tbv& dst, uint64 n, unsigned hi, unsigned lo);
+    void set(tbv& dst, rational const& r, unsigned hi, unsigned lo);
+    void set(tbv& dst, tbv const& other, unsigned hi, unsigned lo);
+    void set(tbv& dst, unsigned index, tbit value);
+
 
     static void debug_alloc();
 };
@@ -99,20 +104,13 @@ public:
         }
     };
         
-    void set(uint64 n, unsigned hi, unsigned lo);
-    void set(rational const& r, unsigned hi, unsigned lo);
-    void set(tbv const& other, unsigned hi, unsigned lo);
 
     tbit operator[](unsigned idx) const { return (tbit)get(idx); }
-    void set(unsigned index, tbit value) {
-        SASSERT(value <= 3);
-        fixed_bit_vector::set(2*index,   (value & 2) != 0);
-        fixed_bit_vector::set(2*index+1, (value & 1) != 0);
-    }
 
 
 private:
 
+
     unsigned get(unsigned index) const {
         index *= 2;
         return (fixed_bit_vector::get(index) << 1) | (unsigned)fixed_bit_vector::get(index+1);
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 110c75ef4..fd3bf1415 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -49,7 +49,7 @@ namespace datalog {
             SASSERT(bv_size == column_num_bits(i));
             unsigned lo = column_idx(i);
             unsigned hi = column_idx(i + 1);
-            d->pos().set(val, hi, lo);
+            dm.tbvm().set(d->pos(),val, hi-1, lo);
         }
         return d;
     }
@@ -311,8 +311,8 @@ namespace datalog {
             utbv& neg = d->neg();
             unsigned mid = dm1.num_tbits();
             unsigned hi  = dm.num_tbits();
-            pos.set(d1.pos(), mid-1, 0);
-            pos.set(d2.pos(), hi-1, mid);
+            dm.tbvm().set(pos,d1.pos(), mid-1, 0);
+            dm.tbvm().set(pos,d2.pos(), hi-1, mid);
             SASSERT(dm.well_formed(*d));
             // first fix bits
             for (unsigned i = 0; i < m_cols1.size(); ++i) {
@@ -323,10 +323,10 @@ namespace datalog {
 
                 if (v1 == BIT_x) {
                     if (v2 != BIT_x)
-                        pos.set(idx1, v2);
+                        dm.tbvm().set(pos, idx1, v2);
                 } 
                 else if (v2 == BIT_x) {
-                    pos.set(idx2, v1);
+                    dm.tbvm().set(pos, idx2, v1);
                 } 
                 else if (v1 != v2) {
                     // columns don't match
@@ -344,12 +344,12 @@ namespace datalog {
                 if (v1 == BIT_x && v2 == BIT_x) {
                     // add to subtracted TBVs: 1xx0 and 0xx1
                     t = dm.tbvm().allocate(pos);
-                    t->set(idx1, BIT_0);
-                    t->set(idx2, BIT_1);
+                    dm.tbvm().set(*t, idx1, BIT_0);
+                    dm.tbvm().set(*t, idx2, BIT_1);
                     neg.push_back(t.detach());                    
                     t = dm.tbvm().allocate(pos);
-                    t->set(idx1, BIT_1);
-                    t->set(idx2, BIT_0);
+                    dm.tbvm().set(*t, idx1, BIT_1);
+                    dm.tbvm().set(*t, idx2, BIT_0);
                     neg.push_back(t.detach());
                 }
                 SASSERT(dm.well_formed(*d));
@@ -358,8 +358,8 @@ namespace datalog {
             // handle subtracted TBVs:  1010 -> 1010xxx
             for (unsigned i = 0; i < d1.neg().size(); ++i) {
                 t = dm.tbvm().allocate();
-                t->set(d1.neg()[i], mid - 1, 0);
-                t->set(d2.pos(),    hi -  1, mid);
+                dm.tbvm().set(*t, d1.neg()[i], mid - 1, 0);
+                dm.tbvm().set(*t, d2.pos(),    hi -  1, mid);
                 if (dm.tbvm().set_and(*t, pos)) {
                     neg.push_back(t.detach());
                 }
@@ -367,8 +367,8 @@ namespace datalog {
             }
             for (unsigned i = 0; i < d2.neg().size(); ++i) {
                 t = dm.tbvm().allocate();
-                t->set(d1.pos(),    mid- 1, 0);
-                t->set(d2.neg()[i], hi - 1, mid);
+                dm.tbvm().set(*t, d1.pos(),    mid- 1, 0);
+                dm.tbvm().set(*t, d2.neg()[i], hi - 1, mid);
                 if (dm.tbvm().set_and(*t, pos)) {
                     neg.push_back(t.detach());
                 }
@@ -637,7 +637,7 @@ namespace datalog {
             unsigned lo = t.column_idx(col);
             unsigned hi = t.column_idx(col+1);
             SASSERT(num_bits == hi - lo);
-            m_filter->pos().set(r, hi-1, lo);
+            dm.tbvm().set(m_filter->pos(), r, hi-1, lo);
         }
         virtual ~filter_equal_fn() {
             dm.deallocate(m_filter);
@@ -743,7 +743,7 @@ namespace datalog {
         }        
         apply_guard(g, result, equalities, discard_cols);
     }
-    bool udoc_relation::apply_eq(expr* g, doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const {
+    bool udoc_relation::apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const {
         udoc_plugin& p = get_plugin();
         unsigned num_bits;
         rational r;
@@ -752,19 +752,65 @@ namespace datalog {
         hi += col;
         if (p.is_numeral(c, r, num_bits)) {
             d = dm.allocateX();
-            d->pos().set(r, hi, lo);
+            dm.tbvm().set(d->pos(), r, hi, lo);
             return true;
         }
         // other cases?
         return false;
     }
 
+    bool udoc_relation::apply_bv_eq(
+        expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const {
+        udoc_plugin& p = get_plugin();
+        ast_manager& m  = p.get_ast_manager();
+        bv_util& bv = p.bv;
+        th_rewriter rw(m);
+        doc_ref d(get_dm());
+        unsigned hi, lo, lo1, lo2, hi1, hi2, v, v1, v2;
+        if (bv.is_concat(e2)) {
+            std::swap(e1, e2);
+        }
+        if (bv.is_concat(e1)) {
+            expr_ref e3(m);
+            app* a1 = to_app(e1);
+            hi = p.num_sort_bits(e1)-1;
+            unsigned n = a1->get_num_args();
+            for (unsigned i = 0; i < n; ++i) {
+                expr* e = a1->get_arg(i);
+                unsigned sz = p.num_sort_bits(e);
+                e3 = bv.mk_extract(hi, hi-sz+1, e2);
+                rw(e3);
+                if (!apply_bv_eq(e, e3, discard_cols, result)) return false;
+                hi -= sz;
+            }
+            return true;
+        }
+        if (is_ground(e1)) {
+            std::swap(e1, e2);
+        }
+        if (is_var_range(e1, hi, lo, v) && is_ground(e2) &&
+            apply_ground_eq(d, v, hi, lo, e2)) {
+            result.intersect(dm, *d);
+            return true;
+        }
+        if (is_var_range(e1, hi1, lo1, v1) && 
+            is_var_range(e2, hi2, lo2, v2)) {
+            unsigned idx1 = lo1 + column_idx(v1);
+            unsigned idx2 = lo2 + column_idx(v2);
+            unsigned length = hi1-lo1+1;
+            result.merge(dm, idx1, idx2, length, discard_cols);
+            return true;
+        }   
+
+        return false;
+    }
+
     void udoc_relation::apply_guard(
         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 *e0, *e1, *e2;
-        unsigned hi, lo, lo1, lo2, hi1, hi2, v, v1, v2;
+        unsigned hi, lo, v;
         doc_ref d(get_dm());
         if (result.is_empty()) {
         }
@@ -781,13 +827,13 @@ namespace datalog {
         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)) {
+                 apply_ground_eq(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)) {
+                 apply_ground_eq(d, v, hi, lo, e2)) {
             result.subtract(dm, *d);
         }
         else if (m.is_not(g, e1)) {
@@ -843,21 +889,9 @@ namespace datalog {
             diff2.reset(dm);
         }
         else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
-            if (is_var_range(e1, hi, lo, v) && is_ground(e2) &&
-                apply_eq(g, d, v, hi, lo, e2)) {
-                result.intersect(dm, *d);
+            if (apply_bv_eq(e1, e2, discard_cols, result)) {
+                // done
             }
-            else if (is_var_range(e2, hi, lo, v) && is_ground(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)) {
-                unsigned idx1 = lo1 + column_idx(v1);
-                unsigned idx2 = lo2 + column_idx(v2);
-                unsigned length = hi1-lo1+1;
-                result.merge(dm, idx1, idx2, length, discard_cols);
-            }   
             else {
                 goto failure_case;
             }            
diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h
index 1d14062e6..64ced8e83 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/src/muz/rel/udoc_relation.h
@@ -70,7 +70,8 @@ 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, doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const;
+        bool apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const;
+        bool apply_bv_eq(expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) 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 409debfb0..2921f52c9 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -117,7 +117,7 @@ class test_doc_cls {
     tbv* mk_rand_tbv() {
         tbv* result = dm.tbvm().allocate();
         for (unsigned i = 0; i < dm.num_tbits(); ++i) {
-            (*result).set(i, choose_tbit());
+            dm.tbvm().set(*result, i, choose_tbit());
         }
         return result;
     }
@@ -126,10 +126,10 @@ class test_doc_cls {
         tbv* result = dm.tbvm().allocate();
         for (unsigned i = 0; i < dm.num_tbits(); ++i) {
             if (pos[i] == BIT_x) {
-                (*result).set(i, choose_tbit());
+                dm.tbvm().set(*result, i, choose_tbit());
             }
             else {
-                (*result).set(i, pos[i]);
+                dm.tbvm().set(*result, i, pos[i]);
             }
         }
         return result;
@@ -159,7 +159,7 @@ class test_doc_cls {
         expr_ref_vector conjs(m);
         for (unsigned i = 0; i < m_vars.size(); ++i) {
             tbit b = choose_tbit();
-            t.set(i, b);            
+            dm.tbvm().set(t, i, b);            
             switch (b) {
             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;
@@ -363,7 +363,7 @@ public:
         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);
+        dm.tbvm().set(*t, 0, BIT_0);
         d->neg().push_back(t.detach());
         unsigned num_bits = dm.num_tbits();
         svector<bool> to_delete(num_bits, false);
@@ -402,10 +402,10 @@ public:
         tbv_ref t2(dm.tbvm());
         t1 = dm.tbvm().allocateX();
         t2 = dm.tbvm().allocateX();
-        t1->set(0, BIT_1);
-        t1->set(2, BIT_0);
-        t2->set(0, BIT_0);
-        t2->set(2, BIT_1);
+        dm.tbvm().set(*t1, 0, BIT_1);
+        dm.tbvm().set(*t1, 2, BIT_0);
+        dm.tbvm().set(*t2, 0, BIT_0);
+        dm.tbvm().set(*t2, 2, BIT_1);
         d1->neg().push_back(t1.detach());
         d1->neg().push_back(t2.detach());
         ds2.push_back(d1.detach());
diff --git a/src/test/fixed_bit_vector.cpp b/src/test/fixed_bit_vector.cpp
index 01d60c347..7bd9e62c3 100644
--- a/src/test/fixed_bit_vector.cpp
+++ b/src/test/fixed_bit_vector.cpp
@@ -28,9 +28,9 @@ static void tst1() {
     fixed_bit_vector_manager m(30);
     fixed_bit_vector *b;
     b = m.allocate0();
-    b->set(0, true);
-    b->set(1, false);
-    b->set(2, true);
+    m.set(*b, 0, true);
+    m.set(*b, 1, false);
+    m.set(*b, 2, true);
     SASSERT(b->get(0) == true);
     SASSERT(b->get(1) == false);
     SASSERT(b->get(2) == true);
@@ -46,19 +46,19 @@ static void tst_or() {
         b1 = m.allocate0();
         b2 = m.allocate0();
 
-        b1->set(4);
-        b2->set(8);
-        b2->set(3);
-        b2->set(2);
-        b2->set(1);
+        m.set(*b1, 4);
+        m.set(*b2, 8);
+        m.set(*b2, 3);
+        m.set(*b2, 2);
+        m.set(*b2, 1);
         m.display(std::cout, *b1) << "\n";
         m.display(std::cout, *b2) << "\n";
         m.set_or(*b1, *b2);
         m.display(std::cout, *b1) << "\n";
         SASSERT(!m.equals(*b1, *b2));
-        b1->unset(4);
+        m.unset(*b1, 4);
         SASSERT(m.equals(*b1, *b2));
-        b1->unset(3);
+        m.unset(*b1, 3);
         SASSERT(!m.equals(*b1, *b2));
         m.deallocate(b1);
         m.deallocate(b2);
@@ -77,16 +77,16 @@ static void tst_eq(unsigned num_bits) {
     fixed_bit_vector* b2 = m.allocate0();
     fixed_bit_vector* b3 = m.allocate0();
 
-    b1->set(3, true);
+    m.set(*b1, 3, true);
     SASSERT(!m.equals(*b1, *b2));
     SASSERT(m.equals(*b2, *b3));
 
-    b3->set(3, true);
+    m.set(*b3, 3, true);
     SASSERT(m.equals(*b1, *b3));
     
-    b2->set(num_bits-1, true);
-    b3->set(num_bits-1);
-    b3->unset(3);
+    m.set(*b2, num_bits-1, true);
+    m.set(*b3, num_bits-1);
+    m.unset(*b3, 3);
     SASSERT(m.equals(*b2, *b3));
     m.fill0(*b1);
     m.set_neg(*b1);
@@ -94,7 +94,7 @@ static void tst_eq(unsigned num_bits) {
     SASSERT(m.equals(*b1, *b2));
     m.fill0(*b1);
     for (unsigned i = 0; i < num_bits; ++i) {
-        b1->set(i, true);
+        m.set(*b1, i, true);
     }
     SASSERT(m.equals(*b1, *b2));
     m.deallocate(b1);
diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp
index 5714c444a..70a07d3f5 100644
--- a/src/test/tbv.cpp
+++ b/src/test/tbv.cpp
@@ -29,8 +29,8 @@ static void tst1(unsigned num_bits) {
     tbv_manager m2(num_bits-2);
     to_delete[1] = true;
     to_delete[3] = true;
-    (*b1).set(2, BIT_0);
-    (*b1).set(4, BIT_x);
+    m.set(*b1, 2, BIT_0);
+    m.set(*b1, 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";
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index 4942164e2..dbe8d9b83 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -54,7 +54,7 @@ class udoc_tester {
     tbv* mk_rand_tbv(doc_manager& dm) {
         tbv* result = dm.tbvm().allocate();
         for (unsigned i = 0; i < dm.num_tbits(); ++i) {
-            (*result).set(i, choose_tbit());
+            dm.tbvm().set(*result, i, choose_tbit());
         }
         return result;
     }
@@ -63,10 +63,10 @@ class udoc_tester {
         tbv* result = dm.tbvm().allocate();
         for (unsigned i = 0; i < dm.num_tbits(); ++i) {
             if (pos[i] == BIT_x) {
-                (*result).set(i, choose_tbit());
+                dm.tbvm().set(*result, i, choose_tbit());
             }
             else {
-                (*result).set(i, pos[i]);
+                dm.tbvm().set(*result, i, pos[i]);
             }
         }
         return result;
diff --git a/src/util/fixed_bit_vector.h b/src/util/fixed_bit_vector.h
index fb7ed38e9..933299925 100644
--- a/src/util/fixed_bit_vector.h
+++ b/src/util/fixed_bit_vector.h
@@ -59,6 +59,7 @@ public:
         return (get_bit_word(bit_idx) & get_pos_mask(bit_idx)) != 0;
     }
     
+private:
     void set(unsigned bit_idx) {
         get_bit_word(bit_idx) |= get_pos_mask(bit_idx);
     }
@@ -116,6 +117,26 @@ public:
     unsigned hash(fixed_bit_vector const& src) const;
     bool contains(fixed_bit_vector const& a, fixed_bit_vector const& b) const;
     std::ostream& display(std::ostream& out, fixed_bit_vector const& b) const;    
+    void set(fixed_bit_vector& dst, unsigned bit_idx) {
+        SASSERT(bit_idx < num_bits());
+        dst.set(bit_idx);
+    }
+    void unset(fixed_bit_vector& dst, unsigned bit_idx) {
+        SASSERT(bit_idx < num_bits());
+        dst.unset(bit_idx);
+    }
+    
+    void set(fixed_bit_vector& dst, unsigned bit_idx, bool val) {
+        SASSERT(bit_idx < num_bits());
+        dst.set(bit_idx, val);
+    }
+
+    // assign bits this[lo:hi] := other[0:hi-lo+1]
+    void set(fixed_bit_vector& dst, fixed_bit_vector const& other, unsigned hi, unsigned lo) {
+        SASSERT(lo <= hi && hi < num_bits());
+        dst.set(other, hi, lo);
+    }
+
 };