diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 9668039cf..e5a6fd97f 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -536,16 +536,15 @@ bool doc_manager::contains(doc const& a, doc const& b) const {
     return true;
 }
 
-bool doc_manager::contains(
-    unsigned offset_a, doc const& a,
-    doc_manager const& dm_b,
-    unsigned offset_b, doc const& b,
-    unsigned length) const {
-    if (!m.contains(offset_a, a.pos(), dm_b.tbvm(), offset_b, b.pos(), length)) return false;
+bool doc_manager::contains(doc const& a, unsigned_vector const& colsa,
+                           doc const& b, unsigned_vector const& colsb) const {
+    if (!m.contains(a.pos(), colsa, b.pos(), colsb))
+        return false;
+
     for (unsigned i = 0; i < a.neg().size(); ++i) {
         bool found = false;
         for (unsigned j = 0; !found && j < b.neg().size(); ++j) {
-            found = dm_b.tbvm().contains(offset_b, b.neg()[j], tbvm(), offset_a, a.neg()[i], length);
+            found = m.contains(b.neg()[j], colsb, a.neg()[i], colsa);
         }
         if (!found) return false;
     }
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index 145f8d456..75b4e9499 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -82,9 +82,8 @@ public:
     bool equals(doc const& a, doc const& b) const;
     unsigned hash(doc const& src) const;
     bool contains(doc const& a, doc const& b) const;
-    bool contains(unsigned offset_a, doc const& a,
-                  doc_manager const& dm_b, unsigned offset_b, doc const& b,
-                  unsigned length) const;
+    bool contains(doc const& a, unsigned_vector const& colsa,
+                  doc const& b, unsigned_vector const& colsb) const;
     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(); }
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 8e213fadc..9c71b826c 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -245,18 +245,12 @@ bool tbv_manager::contains(tbv const& a, tbv const& b) const {
     return m.contains(a, b);
 }
 
-bool tbv_manager::contains(unsigned offset_a, tbv const& a,
-                           tbv_manager const& dm_b, unsigned offset_b, tbv const& b,
-                           unsigned length) const {
-    if (this == &dm_b && length == num_tbits()) {
-        SASSERT(offset_a == 0);
-        SASSERT(offset_b == 0);
-        return m.contains(a, b);
-    }
-    for (unsigned i = 0; i < length; ++i) {
-        tbit bit_a = a[offset_a + i];
+bool tbv_manager::contains(tbv const& a, unsigned_vector const& colsa,
+                           tbv const& b, unsigned_vector const& colsb) const {
+    for (unsigned i = 0; i < colsa.size(); ++i) {
+        tbit bit_a = a[colsa[i]];
         if (bit_a == BIT_x) continue;
-        if (bit_a != b[offset_b + i]) return false;
+        if (bit_a != b[colsb[i]]) return false;
     }
     return true;
 }
diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
index 39067c64c..941853a1b 100644
--- a/src/muz/rel/tbv.h
+++ b/src/muz/rel/tbv.h
@@ -70,9 +70,8 @@ public:
     bool equals(tbv const& a, tbv const& b) const;
     unsigned hash(tbv const& src) const;
     bool contains(tbv const& a, tbv const& b) const;
-    bool contains(unsigned offset_a, tbv const& a,
-                  tbv_manager const& dm_b, unsigned offset_b, tbv const& b,
-                  unsigned length) const;
+    bool contains(tbv const& a, unsigned_vector const& colsa,
+                  tbv const& b, unsigned_vector const& colsb) const;
     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;
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 459b94101..10c01ccdd 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -1064,14 +1064,16 @@ namespace datalog {
     // 4. Unit/stress test cases are needed.
     // 
     class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn {
-        const unsigned_vector m_t_cols;
-        const unsigned_vector m_neg_cols;
+        unsigned_vector m_t_cols;
+        unsigned_vector m_neg_cols;
 
     public:
         negation_filter_fn(const udoc_relation & r, const udoc_relation & neg, unsigned joined_col_cnt,
                            const unsigned *t_cols, const unsigned *neg_cols)
             : m_t_cols(joined_col_cnt, t_cols), m_neg_cols(joined_col_cnt, neg_cols) {
             SASSERT(joined_col_cnt > 0);
+            r.expand_column_vector(m_t_cols);
+            neg.expand_column_vector(m_neg_cols);
         }
         
         virtual void operator()(relation_base& tb, const relation_base& negb) {
@@ -1086,30 +1088,16 @@ namespace datalog {
 
             udoc result;
             for (unsigned i = 0; i < dst.size(); ++i) {
+                bool subsumed = false;
                 for (unsigned j = 0; j < neg.size(); ++j) {
-                    for (unsigned c = 0; c < m_t_cols.size(); ++c) {
-                        unsigned t_col = m_t_cols[c];
-                        unsigned n_col = m_neg_cols[c];
-                        unsigned num_bits = t.column_num_bits(t_col);
-                        SASSERT(num_bits == n.column_num_bits(n_col));
-                        unsigned t_idx = t.column_idx(t_col);
-                        unsigned n_idx = n.column_idx(n_col);
-                        bool cont = dmn.contains(n_idx, neg[j], dmt, t_idx, dst[i], num_bits);
-                        IF_VERBOSE(
-                            3, 
-                            dmt.display(verbose_stream() << "dst:", dst[i], t_idx+num_bits-1,t_idx) << "\n";
-                            dmn.display(verbose_stream() << "neg:", neg[j], n_idx+num_bits-1,n_idx) << "\n";
-                            verbose_stream() << "contains: " << (cont?"true":"false") << "\n";);
-                        if (!cont) {
-                            goto next_neg_disj;
-                        }
+                    if (dmn.contains(neg[j], m_neg_cols, dst[i], m_t_cols)) {
+                        dmt.deallocate(&dst[i]);
+                        subsumed = true;
+                        break;
                     }
-                    dmt.deallocate(&dst[i]);
-                    goto next_disj;
-                next_neg_disj:;
                 }
-                result.push_back(&dst[i]);
-            next_disj:;
+                if (!subsumed)
+                    result.push_back(&dst[i]);
             }
             std::swap(dst, result);
             if (dst.is_empty()) {
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index 523d4e4db..094e755ac 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -148,6 +148,7 @@ public:
 
         test_rename();
         test_filter_neg();
+        test_filter_neg2();
 
 
         // empty
@@ -551,6 +552,55 @@ public:
         t2->deallocate();
     }
 
+    void test_filter_neg2() {
+        // filter_by_negation
+        relation_signature sig4;
+        sig4.push_back(bv.mk_sort(1));
+        sig4.push_back(bv.mk_sort(1));
+        sig4.push_back(bv.mk_sort(1));
+        unsigned_vector cols, allcols;
+
+        cols.push_back(0);
+        cols.push_back(2);
+        allcols.push_back(0);
+        allcols.push_back(1);
+        allcols.push_back(2);
+
+        /// xxx \ 1x0
+        udoc_relation* t1 = mk_full(sig4);
+        {
+            udoc_relation* neg = mk_full(sig4);
+            doc& n = neg->get_udoc()[0];
+            neg->get_dm().set(n, 0, BIT_1);
+            neg->get_dm().set(n, 2, BIT_0);
+            apply_filter_neg(*t1, *neg, allcols, allcols);
+            neg->deallocate();
+        }
+
+        /// xxx \ (1x1 u 0x0)
+        udoc_relation* t2 = mk_full(sig4);
+        {
+            udoc_relation* neg = mk_full(sig4);
+            doc& n = neg->get_udoc()[0];
+            neg->get_dm().set(n, 0, BIT_0);
+            neg->get_dm().set(n, 2, BIT_0);
+            apply_filter_neg(*t2, *neg, allcols, allcols);
+            neg->deallocate();
+        }
+        {
+            udoc_relation* neg = mk_full(sig4);
+            doc& n = neg->get_udoc()[0];
+            neg->get_dm().set(n, 0, BIT_1);
+            neg->get_dm().set(n, 2, BIT_1);
+            apply_filter_neg(*t2, *neg, allcols, allcols);
+            neg->deallocate();
+        }
+
+        apply_filter_neg(*t2, *t1, cols, cols);
+        t1->deallocate();
+        t2->deallocate();
+    }
+
     void set_random(udoc_relation& r, unsigned num_vals) {
         unsigned num_bits = r.get_dm().num_tbits();
         udoc_relation* full = mk_full(r.get_signature());