diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index d73f8c4ad..204a8f316 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -33,7 +33,6 @@ namespace datalog {
 
     void compiler::reset() {
         m_pred_regs.reset();
-        m_new_reg = 0;
     }
 
     void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) {
@@ -51,16 +50,16 @@ namespace datalog {
     }
 
     void compiler::make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, 
-            instruction_block & acc) {
+            bool reuse_t1, instruction_block & acc) {
         relation_signature res_sig;
         relation_signature::from_join(m_reg_signatures[t1], m_reg_signatures[t2], vars.size(), 
             vars.get_cols1(), vars.get_cols2(), res_sig);
-        result = get_fresh_register(res_sig);
+        result = get_register(res_sig, reuse_t1, t1);
         acc.push_back(instruction::mk_join(t1, t2, vars.size(), vars.get_cols1(), vars.get_cols2(), result));
     }
 
     void compiler::make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, 
-            const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) {
+            const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc) {
         relation_signature aux_sig;
         relation_signature sig1 = m_reg_signatures[t1];
         relation_signature sig2 = m_reg_signatures[t2];
@@ -68,29 +67,29 @@ namespace datalog {
         relation_signature res_sig;
         relation_signature::from_project(aux_sig, removed_cols.size(), removed_cols.c_ptr(), 
             res_sig);
-        result = get_fresh_register(res_sig);
+        result = get_register(res_sig, reuse_t1, t1);
 
         acc.push_back(instruction::mk_join_project(t1, t2, vars.size(), vars.get_cols1(), 
             vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
     }
 
     void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
-            const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) {
+            const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc) {
         SASSERT(!removed_cols.empty());
         relation_signature res_sig;
         relation_signature::from_project(m_reg_signatures[src], removed_cols.size(),
             removed_cols.c_ptr(), res_sig);
-        result = get_fresh_register(res_sig);
+        result = get_register(res_sig, reuse, src);
 
         acc.push_back(instruction::mk_filter_interpreted_and_project(src, cond,
             removed_cols.size(), removed_cols.c_ptr(), result));
     }
 
     void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
-            reg_idx & result, instruction_block & acc) {
+            reg_idx & result, bool reuse, instruction_block & acc) {
         relation_signature res_sig;
         relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig);
-        result = get_fresh_register(res_sig);
+        result = get_register(res_sig, reuse, src);
         acc.push_back(instruction::mk_select_equal_and_project(m_context.get_manager(),
             src, val, col, result));
     }
@@ -115,12 +114,12 @@ namespace datalog {
     }
 
     void compiler::make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, 
-            reg_idx & result, instruction_block & acc) {
+            reg_idx & result, bool reuse, instruction_block & acc) {
         SASSERT(col_cnt>0);
 
         relation_signature res_sig;
         relation_signature::from_project(m_reg_signatures[src], col_cnt, removed_cols, res_sig);
-        result = get_fresh_register(res_sig);
+        result = get_register(res_sig, reuse, src);
         acc.push_back(instruction::mk_projection(src, col_cnt, removed_cols, result));
     }
 
@@ -132,6 +131,14 @@ namespace datalog {
         return result;
     }
 
+    compiler::reg_idx compiler::get_register(const relation_signature & sig, bool reuse, compiler::reg_idx r) {
+        if (!reuse)
+            return get_fresh_register(sig);
+        SASSERT(r != execution_context::void_register);
+        m_reg_signatures[r] = sig;
+        return r;
+    }
+
     compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) {
         relation_signature singl_sig;
         singl_sig.push_back(s);
@@ -169,11 +176,11 @@ namespace datalog {
         }
         if(src==execution_context::void_register) {
             result = singleton_table;
-            dealloc = false;
+            SASSERT(dealloc == false);
         }
         else {
             variable_intersection empty_vars(m_context.get_manager());
-            make_join(src, singleton_table, empty_vars, result, acc);
+            make_join(src, singleton_table, empty_vars, result, dealloc, acc);
             dealloc = true;
         }
     }
@@ -198,11 +205,11 @@ namespace datalog {
         }       
         if(src == execution_context::void_register) {
             result = total_table;
-            dealloc = false;
+            SASSERT(dealloc == false);
         }
         else {
             variable_intersection empty_vars(m_context.get_manager());
-            make_join(src, total_table, empty_vars, result, acc);
+            make_join(src, total_table, empty_vars, result, dealloc, acc);
             dealloc = true;
         }
     }
@@ -221,7 +228,7 @@ namespace datalog {
 
 
     void compiler::make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, 
-            instruction_block & acc) {
+            bool reuse, instruction_block & acc) {
 
         relation_signature & src_sig = m_reg_signatures[src];
         reg_idx single_col_reg;
@@ -236,19 +243,20 @@ namespace datalog {
                     removed_cols.push_back(i);
                 }
             }
-            make_projection(src, removed_cols.size(), removed_cols.c_ptr(), single_col_reg, acc);
+            make_projection(src, removed_cols.size(), removed_cols.c_ptr(), single_col_reg, false, acc);
         }
         variable_intersection vi(m_context.get_manager());
         vi.add_pair(col, 0);
-        make_join(src, single_col_reg, vi, result, acc);
-        make_dealloc_non_void(single_col_reg, acc);
+        make_join(src, single_col_reg, vi, result, reuse, acc);
+        if (src_col_cnt != 1)
+            make_dealloc_non_void(single_col_reg, acc);
     }
 
     void compiler::make_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, 
-            reg_idx & result, instruction_block & acc) {
+            reg_idx & result, bool reuse, instruction_block & acc) {
         relation_signature res_sig;
         relation_signature::from_rename(m_reg_signatures[src], cycle_len, permutation_cycle, res_sig);
-        result = get_fresh_register(res_sig);
+        result = get_register(res_sig, reuse, src);
         acc.push_back(instruction::mk_rename(src, cycle_len, permutation_cycle, result));
     }
 
@@ -301,12 +309,8 @@ namespace datalog {
             new_src_col_offset.push_back(src_cols_to_remove.size());
         }
         if(!src_cols_to_remove.empty()) {
-            reg_idx new_curr;
-            make_projection(curr, src_cols_to_remove.size(), src_cols_to_remove.c_ptr(), new_curr, acc);
-            if (dealloc)
-                make_dealloc_non_void(curr, acc);
+            make_projection(curr, src_cols_to_remove.size(), src_cols_to_remove.c_ptr(), curr, dealloc, acc);
             dealloc = true;
-            curr=new_curr;
             curr_sig = & m_reg_signatures[curr];
 
             //update ACK_BOUND_VAR references
@@ -325,21 +329,15 @@ namespace datalog {
             }
             unsigned bound_column_index;
             if(acis[i].kind!=ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) {
-                reg_idx new_curr;
-                bool new_dealloc;
                 bound_column_index=curr_sig->size();
                 if(acis[i].kind==ACK_CONSTANT) {
-                    make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, new_curr, new_dealloc, acc);
+                    make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, curr, dealloc, acc);
                 }
                 else {
                     SASSERT(acis[i].kind==ACK_UNBOUND_VAR);
-                    make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, new_curr, new_dealloc, acc);
+                    make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, curr, dealloc, acc);
                     handled_unbound.insert(acis[i].var_index,bound_column_index);
                 }
-                if (dealloc)
-                    make_dealloc_non_void(curr, acc);
-                dealloc = new_dealloc;
-                curr=new_curr;
                 curr_sig = & m_reg_signatures[curr];
                 SASSERT(bound_column_index==curr_sig->size()-1);
             }
@@ -357,12 +355,8 @@ namespace datalog {
                 used_cols.insert(col);
                 continue;
             }
-            reg_idx new_curr;
-            make_duplicate_column(curr, col, new_curr, acc);
-            if (dealloc)
-                make_dealloc_non_void(curr, acc);
+            make_duplicate_column(curr, col, curr, dealloc, acc);
             dealloc = true;
-            curr=new_curr;
             curr_sig = & m_reg_signatures[curr];
             unsigned bound_column_index=curr_sig->size()-1;
             SASSERT((*curr_sig)[bound_column_index]==acis[i].domain);
@@ -387,12 +381,8 @@ namespace datalog {
                 SASSERT(permutation.size()<=col_cnt); //this should not be an infinite loop
             } while(next!=i);
 
-            reg_idx new_curr;
-            make_rename(curr, permutation.size(), permutation.c_ptr(), new_curr, acc);
-            if (dealloc)
-                make_dealloc_non_void(curr, acc);
+            make_rename(curr, permutation.size(), permutation.c_ptr(), curr, dealloc, acc);
             dealloc = true;
-            curr=new_curr;
             curr_sig = & m_reg_signatures[curr];
         }
 
@@ -491,10 +481,10 @@ namespace datalog {
             get_local_indexes_for_projection(r, removed_cols);
 
             if(removed_cols.empty()) {
-                make_join(t1_reg, t2_reg, a1a2, single_res, acc);
+                make_join(t1_reg, t2_reg, a1a2, single_res, false, acc);
             }
             else {
-                make_join_project(t1_reg, t2_reg, a1a2, removed_cols, single_res, acc);
+                make_join_project(t1_reg, t2_reg, a1a2, removed_cols, single_res, false, acc);
             }
 
             unsigned rem_index = 0;
@@ -521,11 +511,11 @@ namespace datalog {
             SASSERT(rem_index==rem_sz);
         }
         else if(pt_len==1) {
-            reg_idx t_reg=tail_regs[0];
             app * a = r->get_tail(0);
-            SASSERT(m_reg_signatures[t_reg].size()==a->get_num_args());
+            single_res = tail_regs[0];
+            dealloc = false;
 
-            single_res = t_reg;
+            SASSERT(m_reg_signatures[single_res].size() == a->get_num_args());
 
             unsigned n=a->get_num_args();
             for(unsigned i=0; i<n; i++) {
@@ -533,22 +523,14 @@ namespace datalog {
                 if(is_app(arg)) {
                     app * c = to_app(arg); //argument is a constant
                     SASSERT(m.is_value(c));
-                    reg_idx new_reg;
-                    make_select_equal_and_project(single_res, c, single_res_expr.size(), new_reg, acc);
-                    if(single_res!=t_reg) {
-                        //since single_res is a local register, we deallocate it
-                        make_dealloc_non_void(single_res, acc);
-                    }
-                    single_res = new_reg;
+                    make_select_equal_and_project(single_res, c, single_res_expr.size(), single_res, dealloc, acc);
+                    dealloc = true;
                 }
                 else {
                     SASSERT(is_var(arg));
                     single_res_expr.push_back(arg);
                 }
             }
-            if(single_res==t_reg) {
-                dealloc = false;
-            }
 
         }
         else {
@@ -556,6 +538,7 @@ namespace datalog {
 
             //single_res register should never be used in this case
             single_res=execution_context::void_register;
+            dealloc = false;
         }
 
         add_unbound_columns_for_negation(r, head_pred, single_res, single_res_expr, dealloc, acc);
@@ -635,14 +618,7 @@ namespace datalog {
                 } else {
                     // we have an unbound variable, so we add an unbound column for it
                     relation_sort unbound_sort = m_free_vars[v];
-
-                    reg_idx new_reg;
-                    bool new_dealloc;
-                    make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc);
-                    if (dealloc)
-                        make_dealloc_non_void(filtered_res, acc);
-                    dealloc = new_dealloc;
-                    filtered_res = new_reg;
+                    make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, filtered_res, dealloc, acc);
 
                     src_col = single_res_expr.size();
                     single_res_expr.push_back(m.mk_var(v, unbound_sort));
@@ -655,6 +631,12 @@ namespace datalog {
             }
         }
 
+        // add at least one column for the negative filter
+        if (pt_len != ut_len && filtered_res == execution_context::void_register) {
+            relation_signature empty_signature;
+            make_full_relation(head_pred, empty_signature, filtered_res, acc);
+        }
+
         //enforce negative predicates
         for (unsigned i = pt_len; i<ut_len; i++) {
             app * neg_tail = r->get_tail(i);
@@ -673,14 +655,7 @@ namespace datalog {
                 SASSERT(is_app(e));
                 relation_sort arg_sort;
                 m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort);
-                reg_idx new_reg;
-                bool new_dealloc;
-                make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
-
-                if (dealloc)
-                    make_dealloc_non_void(filtered_res, acc);
-                dealloc = new_dealloc;
-                filtered_res = new_reg;
+                make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), filtered_res, dealloc, acc);
 
                 t_cols.push_back(single_res_expr.size());
                 neg_cols.push_back(i);
@@ -750,12 +725,8 @@ namespace datalog {
                     make_clone(filtered_res, filtered_res, acc);
                 acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed));
             } else {
-                reg_idx new_reg;
                 std::sort(remove_columns.begin(), remove_columns.end());
-                make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, new_reg, acc);
-                if (dealloc)
-                    make_dealloc_non_void(filtered_res, acc);
-                filtered_res = new_reg;
+                make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, filtered_res, dealloc, acc);
             }
             dealloc = true;
         }
@@ -892,7 +863,7 @@ namespace datalog {
         ast_manager& m = m_context.get_manager();
         unsigned pt_len = r->get_positive_tail_size();
         unsigned ut_len = r->get_uninterpreted_tail_size();
-        if (pt_len == ut_len || pt_len == 0) {
+        if (pt_len == ut_len) {
             return;
         }
         // populate negative variables:
@@ -921,13 +892,7 @@ namespace datalog {
             expr* e = it->m_value;
             if (!pos_vars.contains(v)) {
                 single_res_expr.push_back(e);
-                reg_idx new_single_res;
-                bool new_dealloc;
-                make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), new_single_res, new_dealloc, acc);
-                if (dealloc)
-                    make_dealloc_non_void(single_res, acc);
-                dealloc = new_dealloc;
-                single_res = new_single_res;
+                make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), single_res, dealloc, acc);
                 TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";);
             }
         }
diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h
index 92f50eb02..8c33f987c 100644
--- a/src/muz/rel/dl_compiler.h
+++ b/src/muz/rel/dl_compiler.h
@@ -82,9 +82,11 @@ namespace datalog {
             
             relation_sort domain;           // domain of the column
             assembling_column_kind kind;    // "instruction" tag
-            unsigned source_column;         // for ACK_BOUND_VAR
-            unsigned var_index;             // for ACK_UNBOUND_VAR
-            relation_element constant;      // for ACK_CONSTANT
+            union {
+                unsigned source_column;         // for ACK_BOUND_VAR
+                unsigned var_index;             // for ACK_UNBOUND_VAR
+                relation_element constant;      // for ACK_CONSTANT
+            };
         };
 
         class instruction_observer : public instruction_block::instruction_observer {
@@ -111,7 +113,6 @@ namespace datalog {
          */
         instruction_block & m_top_level_code;
         pred2idx m_pred_regs;
-        reg_idx                           m_new_reg;
         vector<relation_signature>        m_reg_signatures;
         obj_pair_map<sort, app, reg_idx>  m_constant_registers;
         obj_pair_map<sort, decl, reg_idx> m_total_registers;
@@ -133,6 +134,7 @@ namespace datalog {
         bool compile_with_widening() const { return m_context.compile_with_widening(); }
 
         reg_idx get_fresh_register(const relation_signature & sig);
+        reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r);
         reg_idx get_single_column_register(const relation_sort & s);
 
         /**
@@ -143,21 +145,21 @@ namespace datalog {
         void get_fresh_registers(const func_decl_set & preds,  pred2idx & regs);
 
         void make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, 
-            instruction_block & acc);
+            bool reuse_t1, instruction_block & acc);
         void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, 
-            const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc);
+            const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc);
         void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
-            const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc);
+            const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc);
         void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
-            reg_idx & result, instruction_block & acc);
+            reg_idx & result, bool reuse, instruction_block & acc);
         /**
            \brief Create add an union or widen operation and put it into \c acc.
         */
         void make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widening, instruction_block & acc);
         void make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, 
-            reg_idx & result, instruction_block & acc);
+            reg_idx & result, bool reuse, instruction_block & acc);
         void make_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, 
-            reg_idx & result, instruction_block & acc);
+            reg_idx & result, bool reuse, instruction_block & acc);
         void make_clone(reg_idx src, reg_idx & result, instruction_block & acc);
 
         /**
@@ -183,7 +185,7 @@ namespace datalog {
         void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr,
                                               bool & dealloc, instruction_block& acc);
         
-        void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, instruction_block & acc);
+        void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, bool reuse, instruction_block & acc);
         
         void ensure_predicate_loaded(func_decl * pred, instruction_block & acc);
 
diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 67e2f1e2b..a27d20c56 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -107,6 +107,13 @@ doc& doc_manager::fillX(doc& src) {
     m.fillX(src.pos());
     return src;
 }
+
+unsigned doc_manager::get_size_estimate_bytes(const doc& d) const {
+    return m.get_size_estimate_bytes(d.pos())
+        + d.neg().get_size_estimate_bytes(m)
+        + sizeof(doc);
+}
+
 bool doc_manager::set_and(doc& dst, doc const& src)  {
     // (A \ B) & (C \ D) = (A & C) \ (B u D)
     if (!m.set_and(dst.pos(), src.pos())) return false;
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index fcb134d9e..ca5af005b 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -87,6 +87,7 @@ 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(); }
+    unsigned get_size_estimate_bytes(const doc& d) const;
     doc* project(doc_manager& dstm, 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);
@@ -326,6 +327,13 @@ public:
         }
     }
 
+    unsigned get_size_estimate_bytes(const M& m) const {
+        unsigned sz = sizeof(T*) * size();
+        for (unsigned i = 0; i < size(); ++i) {
+            sz += m.get_size_estimate_bytes(*m_elems[i]);
+        }
+        return sz;
+    }
 };
 
 
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 4fd9a8fe9..9fa7eadd0 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -172,8 +172,6 @@ namespace datalog {
 
             compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
 
-            TRACE("dl", m_code.display(m_ectx, tout); );
-
             bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
 
             if (time_limit || restart_time!=0) {
@@ -628,11 +626,6 @@ namespace datalog {
         m_code.make_annotations(m_ectx);
         m_code.process_all_costs();  
 
-        out << "\n--------------\n";
-        out << "Instructions\n";
-        m_code.display(m_ectx, out);
-
-        out << "\n--------------\n";
         out << "Big relations\n";
         m_ectx.report_big_relations(1000, out);
 
diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
index d667ccaa2..ad98b8095 100644
--- a/src/muz/rel/tbv.h
+++ b/src/muz/rel/tbv.h
@@ -57,6 +57,8 @@ public:
     tbv* allocate(tbv const& bv, unsigned const* permutation);
 
     void deallocate(tbv* bv);
+
+    unsigned get_size_estimate_bytes(const tbv&) const { return m.num_bytes(); }
         
     void copy(tbv& dst, tbv const& src) const;
     unsigned num_tbits() const { return m.num_bits()/2; }
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 90c3ec7c0..8e971ac1e 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -181,6 +181,10 @@ namespace datalog {
         m_elems.display(dm, out); out << "\n";
     }
 
+    unsigned udoc_relation::get_size_estimate_bytes() const {
+        return sizeof(*this) + m_elems.get_size_estimate_bytes(dm);
+    }
+
     // -------------
 
     udoc_plugin::udoc_plugin(relation_manager& rm):
@@ -509,13 +513,27 @@ namespace datalog {
         }
     };
     void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) {
-        for (unsigned i = 0; i < src.size(); ++i) {
-            doc* d = dm.allocate(src[i]);
-            if (dst.insert(dm, d)) {
+        bool deltaempty = delta ? delta->is_empty() : false;
+
+        if (dst.is_empty()) {
+            for (unsigned i = 0; i < src.size(); ++i) {
+                dst.push_back(dm.allocate(src[i]));
                 if (delta) {
-                    delta->insert(dm, dm.allocate(src[i]));
+                    if (deltaempty)
+                        delta->push_back(dm.allocate(src[i]));
+                    else
+                        delta->insert(dm, dm.allocate(src[i]));
                 }
-            } 
+            }
+        } else {
+            for (unsigned i = 0; i < src.size(); ++i) {
+                if (dst.insert(dm, dm.allocate(src[i])) && delta) {
+                    if (deltaempty)
+                        delta->push_back(dm.allocate(src[i]));
+                    else
+                        delta->insert(dm, dm.allocate(src[i]));
+                }
+            }
         }
     }
     relation_union_fn * udoc_plugin::mk_union_fn(
diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h
index a9d31e7d3..40f2222fc 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/src/muz/rel/udoc_relation.h
@@ -53,6 +53,7 @@ namespace datalog {
         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(); }
+        virtual unsigned get_size_estimate_bytes() const;
 
         doc_manager& get_dm() const { return dm; }
         udoc const& get_udoc() const { return m_elems; }
diff --git a/src/util/debug.h b/src/util/debug.h
index a36743f73..f7383511b 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -58,12 +58,18 @@ bool is_debug_enabled(const char * tag);
 #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
 
+#ifdef Z3DEBUG
+# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
+#else
 #if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable)
 // only available in gcc >= 4.5 and in newer versions of clang
 # define UNREACHABLE() __builtin_unreachable()
+#elif defined(_MSC_VER)
+# define UNREACHABLE() __assume(0)
 #else
 #define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
 #endif
+#endif
 
 #define NOT_IMPLEMENTED_YET() { std::cerr << "NOT IMPLEMENTED YET!\n"; UNREACHABLE(); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)