diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index d37e9cca8..9e8789aa6 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -233,7 +233,7 @@ namespace datalog {
         m_engine_type(LAST_ENGINE),
         m_cancel(false) {
         re.set_context(this);
-        m_generate_proof_trace = m_params->generate_proof_trace();
+        updt_params(pa);
     }
 
     context::~context() {
@@ -285,7 +285,8 @@ namespace datalog {
     unsigned context::dl_profile_milliseconds_threshold() const { return m_params->datalog_profile_timeout_milliseconds(); }
     bool context::all_or_nothing_deltas() const { return m_params->datalog_all_or_nothing_deltas(); }
     bool context::compile_with_widening() const { return m_params->datalog_compile_with_widening(); }
-    bool context::unbound_compressor() const { return m_params->datalog_unbound_compressor(); }
+    bool context::unbound_compressor() const { return m_unbound_compressor; }
+    void context::set_unbound_compressor(bool f) { m_unbound_compressor = f; }
     bool context::similarity_compressor() const { return m_params->datalog_similarity_compressor(); }
     unsigned context::similarity_compressor_threshold() const { return m_params->datalog_similarity_compressor_threshold(); }
     unsigned context::soft_timeout() const { return m_fparams.m_soft_timeout; }
@@ -293,8 +294,7 @@ namespace datalog {
     bool context::generate_explanations() const { return m_params->datalog_generate_explanations(); }
     bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); }
     bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries();  }
-    bool context::eager_emptiness_checking() const { return m_params->datalog_eager_emptiness_checking(); }
-
+    
     bool context::bit_blast() const { return m_params->xform_bit_blast(); }
     bool context::karr() const { return m_params->xform_karr(); }
     bool context::scale() const { return m_params->xform_scale(); }
@@ -839,6 +839,7 @@ namespace datalog {
         m_params_ref.copy(p);
         if (m_engine.get()) m_engine->updt_params();
         m_generate_proof_trace = m_params->generate_proof_trace();
+        m_unbound_compressor = m_params->datalog_unbound_compressor(); 
     }
 
     expr_ref context::get_background_assertion() {
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index fb49f02bc..0b9c623c4 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -172,6 +172,7 @@ namespace datalog {
         params_ref         m_params_ref;
         fixedpoint_params*  m_params;
         bool               m_generate_proof_trace;
+        bool               m_unbound_compressor;
         dl_decl_util       m_decl_util;
         th_rewriter        m_rewriter;
         var_subst          m_var_subst;
@@ -256,6 +257,7 @@ namespace datalog {
         bool all_or_nothing_deltas() const;
         bool compile_with_widening() const;
         bool unbound_compressor() const;
+        void set_unbound_compressor(bool f);
         bool similarity_compressor() const;
         unsigned similarity_compressor_threshold() const;
         unsigned soft_timeout() const;
@@ -263,7 +265,6 @@ namespace datalog {
         bool generate_explanations() const;
         bool explanations_on_relation_level() const;
         bool magic_sets_for_queries() const;
-        bool eager_emptiness_checking() const;
         bool bit_blast() const;
         bool karr() const;
         bool scale() const;
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index d61c442d3..7951a62bc 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -33,9 +33,6 @@ def_module_params('fixedpoint',
                            "updated relation was modified or not"),
                           ('datalog.compile_with_widening', BOOL, False, 
                            "widening will be used to compile recursive rules"),
-                          ('datalog.eager_emptiness_checking', BOOL, True, 
-                           "emptiness of affected relations will be checked after each instruction, " +
-                           "so that we may ommit unnecessary instructions"),
                           ('datalog.default_table_checked', BOOL, False, "if true, the detault " +
                            'table will be default_table inside a wrapper that checks that its results ' +
                            'are the same as of default_table_checker table'),
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index d03c94154..e53dae88a 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -465,6 +465,14 @@ namespace datalog {
             relation_manager & get_manager() const { return get_plugin().get_manager(); }
 
             virtual bool empty() const = 0;
+            /**
+               \brief fast emptiness check. This may be partial.
+               The requirement is that if fast_empty returns true 
+               then the table or relation is in fact empty.
+               It is allowed to return false even if the relation is non-empty.
+            */
+            virtual bool fast_empty() const { return empty(); }
+
             virtual void add_fact(const fact & f) = 0;
             /**
                \brief Like \c add_fact, only here the caller guarantees that the fact is not present in
diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index 1dfdf96b9..f8eadfed3 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -37,8 +37,7 @@ namespace datalog {
     execution_context::execution_context(context & context) 
         : m_context(context),
         m_stopwatch(0),
-        m_timelimit_ms(0),
-        m_eager_emptiness_checking(context.eager_emptiness_checking()) {}
+        m_timelimit_ms(0) {}
 
     execution_context::~execution_context() {
         reset();
@@ -122,6 +121,22 @@ namespace datalog {
              m_timelimit_ms < static_cast<unsigned>(1000*m_stopwatch->get_current_seconds()));
     }
 
+    void execution_context::collect_statistics(statistics& st) const {
+        st.update("dl.joins",   m_stats.m_join);
+        st.update("dl.project", m_stats.m_project);
+        st.update("dl.filter",  m_stats.m_filter);
+        st.update("dl.total", m_stats.m_total);
+        st.update("dl.unary_singleton", m_stats.m_unary_singleton);
+        st.update("dl.filter_by_negation", m_stats.m_filter_by_negation);
+        st.update("dl.select_equal_project", m_stats.m_select_equal_project);
+        st.update("dl.join_project", m_stats.m_join_project);
+        st.update("dl.project_rename", m_stats.m_project_rename);
+        st.update("dl.union", m_stats.m_union);
+        st.update("dl.filter_interpreted_project", m_stats.m_filter_interp_project);
+        st.update("dl.filter_id", m_stats.m_filter_id);
+        st.update("dl.filter_eq", m_stats.m_filter_eq);
+    }
+
 
     // -----------------------------------
     //
@@ -182,7 +197,7 @@ namespace datalog {
             }
             else {
                 relation_base& rel = ctx.get_rel_context().get_relation(m_pred);
-                if ((!ctx.eager_emptiness_checking() || !rel.empty())) {
+                if (!rel.fast_empty()) {
                     ctx.set_reg(m_reg, rel.clone());
                 }
                 else {
@@ -348,6 +363,7 @@ namespace datalog {
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
             ctx.make_empty(m_res);
+            ++ctx.m_stats.m_join;
             if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
                 return true;
             }
@@ -375,7 +391,7 @@ namespace datalog {
                 ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);
                 tout<<":"<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";);
 
-            if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
+            if (ctx.reg(m_res)->fast_empty()) {
                 ctx.make_empty(m_res);
             }
             return true;
@@ -409,6 +425,7 @@ namespace datalog {
             : m_reg(reg), m_value(value, m), m_col(col) {}
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
+            ++ctx.m_stats.m_filter_eq;
             if (!ctx.reg(m_reg)) {
                 return true;
             }
@@ -426,7 +443,7 @@ namespace datalog {
             }
             (*fn)(r);
 
-            if (ctx.eager_emptiness_checking() && r.empty()) {
+            if (r.fast_empty()) {
                 ctx.make_empty(m_reg);
             }
             return true;
@@ -457,6 +474,7 @@ namespace datalog {
             : m_reg(reg), m_cols(col_cnt, identical_cols) {}
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
+            ++ctx.m_stats.m_filter_id;
             if (!ctx.reg(m_reg)) {
                 return true;
             }
@@ -474,7 +492,7 @@ namespace datalog {
             }
             (*fn)(r);
 
-            if (ctx.eager_emptiness_checking() && r.empty()) {
+            if (r.fast_empty()) {
                 ctx.make_empty(m_reg);
             }
             return true;
@@ -504,6 +522,7 @@ namespace datalog {
                 return true;
             }
             log_verbose(ctx);            
+            ++ctx.m_stats.m_filter;
 
             relation_mutator_fn * fn;
             relation_base & r = *ctx.reg(m_reg);
@@ -519,7 +538,7 @@ namespace datalog {
             }
             (*fn)(r);
 
-            if (ctx.eager_emptiness_checking() && r.empty()) {
+            if (r.fast_empty()) {
                 ctx.make_empty(m_reg);
             }            
             TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n"););
@@ -559,6 +578,7 @@ namespace datalog {
                 ctx.make_empty(m_res);
                 return true;
             }
+            ++ctx.m_stats.m_filter_interp_project;
 
             relation_transformer_fn * fn;
             relation_base & reg = *ctx.reg(m_src);
@@ -575,7 +595,7 @@ namespace datalog {
 
             ctx.set_reg(m_res, (*fn)(reg));
 
-            if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
+            if (ctx.reg(m_res)->fast_empty()) {
                 ctx.make_empty(m_res);
             }
             TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n"););
@@ -613,12 +633,13 @@ namespace datalog {
         instr_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widen)
             : m_src(src), m_tgt(tgt), m_delta(delta), m_widen(widen) {}
         virtual bool perform(execution_context & ctx) {
-            log_verbose(ctx);            
             TRACE("dl", tout << "union " << m_src << " into " << m_tgt 
                   << " " << ctx.reg(m_src) << " " << ctx.reg(m_tgt) << "\n";);
             if (!ctx.reg(m_src)) {
                 return true;
             }
+            log_verbose(ctx);            
+            ++ctx.m_stats.m_union;
             relation_base & r_src = *ctx.reg(m_src);
             if (!ctx.reg(m_tgt)) {
                 relation_base * new_tgt = r_src.get_plugin().mk_empty(r_src);
@@ -682,7 +703,7 @@ namespace datalog {
                     r_delta->display(tout <<"delta:");
                 });
 
-            if (ctx.eager_emptiness_checking() && r_delta && r_delta->empty()) {
+            if (r_delta && r_delta->fast_empty()) {
                 ctx.make_empty(m_delta);
             }
 
@@ -726,11 +747,12 @@ namespace datalog {
             reg_idx tgt) : m_projection(projection), m_src(src), 
             m_cols(col_cnt, cols), m_tgt(tgt) {}
         virtual bool perform(execution_context & ctx) {
-            log_verbose(ctx);            
             ctx.make_empty(m_tgt);
             if (!ctx.reg(m_src)) {
                 return true;
             }
+            log_verbose(ctx);            
+            ++ctx.m_stats.m_project_rename;
 
             relation_transformer_fn * fn;
             relation_base & r_src = *ctx.reg(m_src);
@@ -797,6 +819,7 @@ namespace datalog {
             if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
                 return true;
             }
+            ++ctx.m_stats.m_join_project;
             relation_join_fn * fn;
             const relation_base & r1 = *ctx.reg(m_rel1);
             const relation_base & r2 = *ctx.reg(m_rel2);
@@ -811,7 +834,7 @@ namespace datalog {
             TRACE("dl", tout<<r1.get_size_estimate_rows()<<" x "<<r2.get_size_estimate_rows()<<" jp->\n";);
             ctx.set_reg(m_res, (*fn)(r1, r2));
             TRACE("dl",  tout<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";);
-            if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
+            if (ctx.reg(m_res)->fast_empty()) {
                 ctx.make_empty(m_res);
             }
             return true;
@@ -855,6 +878,7 @@ namespace datalog {
 
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
+            ++ctx.m_stats.m_select_equal_project;
             if (!ctx.reg(m_src)) {
                 ctx.make_empty(m_result);
                 return true;
@@ -873,7 +897,7 @@ namespace datalog {
             }
             ctx.set_reg(m_result, (*fn)(r));
 
-            if (ctx.eager_emptiness_checking() && ctx.reg(m_result)->empty()) {
+            if (ctx.reg(m_result)->fast_empty()) {
                 ctx.make_empty(m_result);
             }
             return true;
@@ -913,6 +937,8 @@ namespace datalog {
             if (!ctx.reg(m_tgt) || !ctx.reg(m_neg_rel)) {
                 return true;
             }
+            ++ctx.m_stats.m_filter_by_negation;
+
             relation_intersection_filter_fn * fn;
             relation_base & r1 = *ctx.reg(m_tgt);
             const relation_base & r2 = *ctx.reg(m_neg_rel);
@@ -928,7 +954,7 @@ namespace datalog {
             }
             (*fn)(r1, r2);
 
-            if (ctx.eager_emptiness_checking() && r1.empty()) {
+            if (r1.fast_empty()) {
                 ctx.make_empty(m_tgt);
             }
             return true;
@@ -966,6 +992,7 @@ namespace datalog {
         }
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
+            ++ctx.m_stats.m_unary_singleton;
             ctx.make_empty(m_tgt);
             relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
             rel->add_fact(m_fact);
@@ -999,6 +1026,7 @@ namespace datalog {
         instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {}
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
+            ++ctx.m_stats.m_total;
             ctx.make_empty(m_tgt);
             ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred));
             return true;
diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h
index b816f9e55..87f9df19f 100644
--- a/src/muz/rel/dl_instruction.h
+++ b/src/muz/rel/dl_instruction.h
@@ -66,14 +66,6 @@ namespace datalog {
         reg_annotations     m_reg_annotation;
         stopwatch *         m_stopwatch;
         unsigned            m_timelimit_ms; //zero means no limit
-        /**
-           \brief If true, after every operation that may result in an empty relation, a check
-           for emptiness will be performed, and if a relation is empty, it will be deleted
-           and replaced by zero. This allows us to avoid performing operations that would have
-           no effect due to relation emptiness, but if the check for emptiness is expensive, its
-           cost may overcome the gains.
-         */
-        bool                m_eager_emptiness_checking;
     public:
         execution_context(context & context);
         ~execution_context();
@@ -86,7 +78,26 @@ namespace datalog {
         void reset_timelimit();
         bool should_terminate();
 
-        bool eager_emptiness_checking() const { return m_eager_emptiness_checking; }
+        struct stats {
+            unsigned m_join;
+            unsigned m_project;
+            unsigned m_filter;
+            unsigned m_total;
+            unsigned m_unary_singleton;
+            unsigned m_filter_by_negation;
+            unsigned m_select_equal_project;
+            unsigned m_join_project;
+            unsigned m_project_rename;
+            unsigned m_union;
+            unsigned m_filter_interp_project;
+            unsigned m_filter_id;
+            unsigned m_filter_eq;
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+        stats m_stats;
+
+        void collect_statistics(statistics& st) const;
 
         /**
            \brief Return reference to \c i -th register that contains pointer to a relation.
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index a4c254272..e227e469a 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -538,7 +538,7 @@ namespace datalog {
         for(; it!=end; ++it) {
             func_decl * pred = *it;
             relation_base * rel = try_get_relation(pred);
-            if(!rel) {
+            if (!rel) {
                 out << "Tuples in " << pred->get_name() << ": \n";
                 continue;
             }
diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 6ddc5b6b4..927eed283 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -434,6 +434,34 @@ bool doc_manager::equals(doc const& a, doc const& b) const {
 bool doc_manager::is_full(doc const& src) const {
     return src.neg().is_empty() && m.equals(src.pos(), *m_full);
 }
+bool doc_manager::is_empty(doc const& src)  {
+    if (src.neg().size() == 0) return false;
+    if (src.neg().size() == 1) {
+        return m.equals(src.pos(), src.neg()[0]);
+    }
+    tbv_ref pos(m, m.allocate(src.pos()));
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        bool found = false;
+        for (unsigned j = 0; !found && j < num_tbits(); ++j) {
+            tbit b1 = (*pos)[j];
+            tbit b2 = src.neg()[i][j];
+            found = (b1 != BIT_x && b2 != BIT_x && b1 != b2);
+        }
+        for (unsigned j = 0; !found && j < num_tbits(); ++j) {
+            tbit b1 = (*pos)[j];
+            tbit b2 = src.neg()[i][j];
+            found = (b1 == BIT_x && b2 != BIT_x);
+            if (found) {
+                pos->set(j, neg(b2));
+            }
+        }
+        if (!found) {
+            return false; // TBD make complete SAT check.
+        }
+    }
+    return true;
+}
+
 unsigned doc_manager::hash(doc const& src) const {
     unsigned r = 0;
     for (unsigned i = 0; i < src.neg().size(); ++i) {
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index b29ecb7c6..bf2cdc229 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -57,6 +57,7 @@ public:
     doc& fill1(doc& src);
     doc& fillX(doc& src);
     bool is_full(doc const& src) const;
+    bool is_empty(doc const& src);
     bool set_and(doc& dst, doc const& src);
     bool fold_neg(doc& dst);
     bool intersect(doc const& A, doc const& B, doc& result);
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 920a0924a..13aecbe09 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -222,6 +222,7 @@ namespace datalog {
     }
  
     lbool rel_context::query(unsigned num_rels, func_decl * const* rels) {
+        setup_default_relation();
         get_rmanager().reset_saturated_marks();
         scoped_query _scoped_query(m_context);
         for (unsigned i = 0; i < num_rels; ++i) {
@@ -307,6 +308,7 @@ namespace datalog {
     }
 
     lbool rel_context::query(expr* query) {
+        setup_default_relation();
         get_rmanager().reset_saturated_marks();
         scoped_query _scoped_query(m_context);
         rule_manager& rm = m_context.get_rule_manager();
@@ -495,6 +497,12 @@ namespace datalog {
         get_rmanager().set_cancel(f);        
     }
 
+    void rel_context::setup_default_relation() {
+        if (m_context.default_relation() == symbol("doc")) {
+            m_context.set_unbound_compressor(false);
+        }
+    }
+
     relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) {
         relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
         if (!plugin) {
@@ -553,6 +561,10 @@ namespace datalog {
         get_rmanager().store_relation(pred, rel);
     }
 
+    void rel_context::collect_statistics(statistics& st) const {
+        m_ectx.collect_statistics(st);
+    }
+
     void rel_context::inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) {
         if (orig_pred) {
             family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred);            
diff --git a/src/muz/rel/rel_context.h b/src/muz/rel/rel_context.h
index 84b100415..5e26718d6 100644
--- a/src/muz/rel/rel_context.h
+++ b/src/muz/rel/rel_context.h
@@ -52,6 +52,8 @@ namespace datalog {
 
         void set_cancel(bool f);
 
+        void setup_default_relation();
+
     public:
         rel_context(context& ctx);
 
@@ -77,6 +79,7 @@ namespace datalog {
         
         virtual void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred);
 
+        virtual void collect_statistics(statistics& st) const;
 
         virtual void cancel() { set_cancel(true); }
         virtual void cleanup() { set_cancel(false);}
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 458aea9d0..0dcbcade9 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -191,8 +191,17 @@ bool tbv_manager::set_and(tbv& dst,  tbv const& src) const {
 }
 
 bool tbv_manager::is_well_formed(tbv const& dst) const {
-    for (unsigned i = 0; i < num_tbits(); ++i) {
-        if (dst[i] == BIT_z) return false;
+    unsigned nw = m.num_words();
+    unsigned w;
+    for (unsigned i = 0; i + 1 < nw; ++i) {
+        w = dst.get_word(i);
+        w = w | (w << 1) | 0x55555555;
+        if (w != 0xFFFFFFFF) return false;
+    }
+    if (nw > 0) {        
+        w = m.last_word(dst);
+        w = w | (w << 1) | 0x55555555 | ~m.get_mask();
+        if (w != 0xFFFFFFFF) return false;
     }
     return true;
 }
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 17b2ded0c..205d52416 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -57,6 +57,16 @@ namespace datalog {
         doc* d = fact2doc(f);
         m_elems.insert(dm, d);
     }
+    void udoc_relation::add_new_fact(const relation_fact & f) {
+        m_elems.push_back(fact2doc(f));
+    }
+    bool udoc_relation::empty() const {
+        // TBD: make this a complete check
+        for (unsigned i = 0; i < m_elems.size(); ++i) {
+            if (!dm.is_empty(m_elems[i])) return false;
+        }
+        return true;
+    }
     bool udoc_relation::contains_fact(const relation_fact & f) const {
         doc_ref d(dm, fact2doc(f));
         return m_elems.contains(dm, *d);
@@ -240,9 +250,8 @@ namespace datalog {
         unsigned num_bits = 0;
         if (bv.is_bv_sort(s))
             return bv.get_bv_size(s);
-        if (m.is_bool(s)) {
+        if (m.is_bool(s)) 
             return 1;
-        }
         uint64 sz;
         if (dl.try_get_size(s, sz)) {
             while (sz > 0) ++num_bits, sz /= 2;
diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h
index 697928d60..c3ce8d2c4 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/src/muz/rel/udoc_relation.h
@@ -32,7 +32,7 @@ namespace datalog {
     class udoc_relation : public relation_base {
         friend class udoc_plugin;
         doc_manager&    dm;
-        udoc            m_elems;
+        mutable udoc    m_elems;
         unsigned_vector m_column_info;
         doc* fact2doc(relation_fact const& f) const;        
         expr_ref to_formula(tbv const& t) const;
@@ -42,12 +42,14 @@ namespace datalog {
         virtual ~udoc_relation();
         virtual void reset();
         virtual void add_fact(const relation_fact & f);
+        virtual void add_new_fact(const relation_fact & f);
         virtual bool contains_fact(const relation_fact & f) const;
         virtual udoc_relation * clone() const;
         virtual udoc_relation * complement(func_decl*) const;
         virtual void to_formula(expr_ref& fml) const;
         udoc_plugin& get_plugin() const; 
-        virtual bool empty() const { return m_elems.is_empty(); }
+        virtual bool fast_empty() const { return m_elems.is_empty(); }
+        virtual bool empty() const; 
         virtual void display(std::ostream& out) const;
         virtual bool is_precise() const { return true; }
         virtual unsigned get_size_estimate_rows() const { return m_elems.size(); }
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index d3eb24b9a..7dabece2f 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -644,7 +644,8 @@ namespace datalog {
               tout << " num unifiers: " << m_unifiers.size();
               tout << " num positions: " << m_positions.find(e).size() << "\n";
               output_predicate(m_context, to_app(e), tout); tout << "\n";);
-        return true;
+        // stop visitor when we have more than 1 unifier, since that's all we want.
+        return m_unifiers.size() <= 1;
     }
 
     void mk_rule_inliner::visitor::reset(unsigned sz) {
diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp
index 7fab0b56c..5714c444a 100644
--- a/src/test/tbv.cpp
+++ b/src/test/tbv.cpp
@@ -38,6 +38,7 @@ static void tst1(unsigned num_bits) {
     m.deallocate(b1);
     m.deallocate(bX);
     m.deallocate(bN);
+
 }
 
 static void tst0() {
@@ -54,11 +55,30 @@ static void tst0() {
     SASSERT(m.equals(*t1, *t3));
 }
 
+static void tst2(unsigned num_bits) {
+    tbv_manager m(num_bits);
+    tbv_ref t(m), t2(m);
+    for (unsigned i = 0; i < 55; ++i) {
+        t = m.allocate(i);
+        SASSERT(m.is_well_formed(*t));
+        t2 = m.allocate(i+1);
+        VERIFY(!m.set_and(*t2, *t));
+        SASSERT(!m.is_well_formed(*t2));
+    }
+}
+
 void tst_tbv() {
     tst0();
+    
     tst1(31);
     tst1(11);
     tst1(15);
     tst1(16);
     tst1(17);
+
+    tst2(31);
+    tst2(11);
+    tst2(15);
+    tst2(16);
+    tst2(17);
 }
diff --git a/src/util/fixed_bit_vector.h b/src/util/fixed_bit_vector.h
index 11cb91fef..4ada982d0 100644
--- a/src/util/fixed_bit_vector.h
+++ b/src/util/fixed_bit_vector.h
@@ -108,6 +108,7 @@ public:
     fixed_bit_vector& set_or(fixed_bit_vector& dst,  fixed_bit_vector const& src) const;
     fixed_bit_vector& set_neg(fixed_bit_vector& dst) const;
     unsigned last_word(fixed_bit_vector const& bv) const;
+    unsigned get_mask() const { return m_mask; }
     bool equals(fixed_bit_vector const& a, fixed_bit_vector const& b) const;
     unsigned hash(fixed_bit_vector const& src) const;
     bool contains(fixed_bit_vector const& a, fixed_bit_vector const& b) const;