diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h
index 633676ec7..f941ceabc 100644
--- a/src/muz/base/dl_rule_set.h
+++ b/src/muz/base/dl_rule_set.h
@@ -254,6 +254,7 @@ namespace datalog {
 
         void set_output_predicate(func_decl * pred) { m_refs.push_back(pred); m_output_preds.insert(pred); }
         bool is_output_predicate(func_decl * pred) const { return m_output_preds.contains(pred); }
+        void inherit_output_predicate(rule_set const& src, func_decl* pred) { if (src.is_output_predicate(pred) && !is_output_predicate(pred)) set_output_predicate(pred); }
         const func_decl_set & get_output_predicates() const { return m_output_preds; }
         func_decl* get_output_predicate() const { SASSERT(m_output_preds.size() == 1); return *m_output_preds.begin(); }
 
diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp
index 572b689d5..d2c552355 100644
--- a/src/muz/rel/dl_base.cpp
+++ b/src/muz/rel/dl_base.cpp
@@ -377,8 +377,6 @@ namespace datalog {
 
         if (sig.first_functional() == 0) {
             if (empty()) {
-                if (fact.empty())
-                    throw default_exception("empty relations cannot be complemented");
                 res->add_fact(fact);
             }
             return res;
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index 667640051..d1cc8d06f 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -1231,7 +1231,7 @@ namespace datalog {
 
             bool populated() const { return !m_current.empty(); }
             void ensure_populated() const {
-                if(!populated()) {
+                if (!populated()) {
                     get_fact(m_current);
                 }
             }
diff --git a/src/muz/rel/dl_table.cpp b/src/muz/rel/dl_table.cpp
index 054ac9360..45d3d9f47 100644
--- a/src/muz/rel/dl_table.cpp
+++ b/src/muz/rel/dl_table.cpp
@@ -229,7 +229,7 @@ namespace datalog {
     };
 
     bitvector_table::bitvector_table(bitvector_table_plugin & plugin, const table_signature & sig)
-        : table_base(plugin, sig) {
+        : table_base(plugin, sig){
         SASSERT(plugin.can_handle_signature(sig));
 
         m_num_cols = sig.size();
@@ -237,7 +237,7 @@ namespace datalog {
         for (unsigned i = 0; i < m_num_cols; ++i) {            
             unsigned s = static_cast<unsigned>(sig[i]);
             if (s != sig[i] || !is_power_of_two(s)) {
-                  throw default_exception("bit-vector table is specialized to small domains that are powers of two");
+                throw default_exception("bit-vector table is specialized to small domains that are powers of two");
             }
             m_shift.push_back(shift);
             m_mask.push_back(s - 1);
@@ -253,8 +253,8 @@ namespace datalog {
             if (shift >= 32) {
                   throw default_exception("bit-vector table is specialized to small domains that are powers of two");
             }
-            m_bv.reserve(1 << shift);
         }
+        m_bv.reserve(1 << shift);
     }
     
     unsigned bitvector_table::fact2offset(const table_element* f) const {
@@ -274,19 +274,15 @@ namespace datalog {
     }
     
     void bitvector_table::add_fact(const table_fact & f) {
-        if (m_num_cols > 0) {
-            m_bv.set(fact2offset(f.c_ptr()));
-        }
+        m_bv.set(fact2offset(f.c_ptr()));        
     }
 
     void bitvector_table::remove_fact(const table_element* fact) {    
-        if (m_num_cols > 0) {
-            m_bv.unset(fact2offset(fact));
-        }
+        m_bv.unset(fact2offset(fact));        
     }
 
     bool bitvector_table::contains_fact(const table_fact & f) const {
-        return !f.empty() && m_bv.get(fact2offset(f.c_ptr()));
+        return m_bv.get(fact2offset(f.c_ptr()));
     }
 
     table_base::iterator bitvector_table::begin() const {
diff --git a/src/muz/rel/dl_table.h b/src/muz/rel/dl_table.h
index 168108e65..dad4ed079 100644
--- a/src/muz/rel/dl_table.h
+++ b/src/muz/rel/dl_table.h
@@ -127,8 +127,8 @@ namespace datalog {
         friend class bitvector_table_plugin;
 
         class bv_iterator;
-        bit_vector m_bv;
-        unsigned   m_num_cols;
+        bit_vector      m_bv;
+        unsigned        m_num_cols;
         unsigned_vector m_shift;
         unsigned_vector m_mask;
 
diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index a03a9c71e..9182fbc55 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -292,14 +292,16 @@ namespace datalog {
                     rm.mk_rule(fml, pr, *result, r->name());
                 }
                 else {
-                    result->add_rule(r);
+                    result->add_rule(r);     
+                    result->inherit_output_predicate(source, r->get_decl());
                 }
             }
 
             // copy output predicates without any rule (bit-blasting not really needed)
             const func_decl_set& decls = source.get_output_predicates();
             for (func_decl* p : decls)
-                result->set_output_predicate(p);            
+                if (!source.contains(p))
+                    result->set_output_predicate(p);            
 
             if (m_context.get_model_converter()) {
                 generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast");