diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index f8eadfed3..4122811ac 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -156,6 +156,14 @@ namespace datalog {
         process_costs();
     }
 
+    void instruction::collect_statistics(statistics& st) const {
+        costs c;
+        get_total_cost(c);
+        st.update("instruction", c.instructions);
+        st.update("instruction-time", c.milliseconds);
+    }
+
+
     void instruction::display_indented(rel_context_base const & _ctx, std::ostream & out, std::string indentation) const {
         out << indentation;
         rel_context const& ctx = dynamic_cast<const rel_context&>(_ctx);
@@ -257,7 +265,7 @@ namespace datalog {
         instr_clone_move(bool clone, reg_idx src, reg_idx tgt)
             : m_clone(clone), m_src(src), m_tgt(tgt) {}
         virtual bool perform(execution_context & ctx) {
-            log_verbose(ctx);            
+            if (ctx.reg(m_src)) log_verbose(ctx);            
             ctx.make_empty(m_tgt);
             if (m_clone) {
                 ctx.set_reg(m_tgt, ctx.reg(m_src) ? ctx.reg(m_src)->clone() : 0);
@@ -1145,6 +1153,15 @@ namespace datalog {
         }
     }
 
+
+    void instruction_block::collect_statistics(statistics& st) const {
+        instr_seq_type::const_iterator it = m_data.begin();
+        instr_seq_type::const_iterator end = m_data.end();
+        for(; it!=end; ++it) {
+            (*it)->collect_statistics(st);
+        }
+    }
+
     void instruction_block::make_annotations(execution_context & ctx) {
         instr_seq_type::iterator it = m_data.begin();
         instr_seq_type::iterator end = m_data.end();
diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h
index 87f9df19f..331b153e8 100644
--- a/src/muz/rel/dl_instruction.h
+++ b/src/muz/rel/dl_instruction.h
@@ -232,7 +232,7 @@ namespace datalog {
 
            Each line must be prepended by \c indentation and ended by a newline character.
         */
-        virtual void display_body_impl(rel_context const & ctx, std::ostream & out, std::string indentation) const {}
+        virtual void display_body_impl(rel_context_base const & ctx, std::ostream & out, std::string indentation) const {}
         void log_verbose(execution_context& ctx);
 
     public:
@@ -301,6 +301,8 @@ namespace datalog {
 
         static instruction * mk_assert_signature(const relation_signature & s, reg_idx tgt);
 
+        void collect_statistics(statistics& st) const;
+
     };
 
 
@@ -327,7 +329,7 @@ namespace datalog {
 
         void push_back(instruction * i) { 
             m_data.push_back(i);
-            if(m_observer) {
+            if (m_observer) {
                 m_observer->notify(i);
             }
         }
@@ -336,6 +338,8 @@ namespace datalog {
             m_observer = o;
         }
 
+        void collect_statistics(statistics& st) const;
+
         /**
            \brief Perform instructions in the block. If the run was interrupted before completion,
            return false; otherwise return true.
@@ -353,6 +357,8 @@ namespace datalog {
             display_indented(ctx, out, "");
         }
         void display_indented(rel_context_base const & ctx, std::ostream & out, std::string indentation) const;
+
+        unsigned num_instructions() const { return m_data.size(); }
     };
 
 
diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index bb9e0e649..917eeb655 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -21,6 +21,10 @@ Revision History:
 --*/
 
 #include "doc.h"
+#include "smt_kernel.h"
+#include "expr_safe_replace.h"
+#include "smt_params.h"
+#include "ast_util.h"
 
 doc_manager::doc_manager(unsigned n): m(n), m_alloc("doc") {
     m_full = m.allocateX();
@@ -384,15 +388,6 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
     return r;
 }
 
-#if 0
-bool doc_manager::can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg) {
-    for (unsigned i = 0; i < n; ++i) {
-        if (to_delete[i] && BIT_x != neg[i] && BIT_x == pos[i]) return false;
-    }
-    return true;
-}
-#endif
-
 doc_manager::project_action_t 
 doc_manager::pick_resolvent(
     tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx) {
@@ -453,7 +448,8 @@ doc_manager::pick_resolvent(
         return project_done;
     }
 }
-    
+
+
 
 void doc_manager::complement(doc const& src, doc_vector& result) {
     result.reset();
@@ -504,6 +500,9 @@ bool doc_manager::is_empty(doc const& src)  {
     if (src.neg().size() == 1) {
         return m.equals(src.pos(), src.neg()[0]);
     }
+    return false;
+#if 0
+    // buggy:
     tbv_ref pos(m, m.allocate(src.pos()));
     for (unsigned i = 0; i < src.neg().size(); ++i) {
         bool found = false;
@@ -525,6 +524,7 @@ bool doc_manager::is_empty(doc const& src)  {
         }
     }
     return true;
+#endif
 }
 
 unsigned doc_manager::hash(doc const& src) const {
@@ -559,3 +559,72 @@ std::ostream& doc_manager::display(std::ostream& out, doc const& b) const {
     return out;
 }
 
+
+void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst) {
+    expr_ref fml1 = to_formula(m, src);
+    expr_ref fml2 = dstm.to_formula(m, dst);
+    project_rename(fml2, to_delete);
+    project_expand(fml1, to_delete);   
+    check_equiv(m, fml1, fml2);
+}
+
+void doc_manager::check_equiv(ast_manager& m, expr* fml1, expr* fml2) {
+    smt_params fp;
+    smt::kernel solver(m, fp);
+    expr_ref fml(m);
+    fml = m.mk_not(m.mk_eq(fml1, fml2));
+    solver.assert_expr(fml);
+    lbool res = solver.check();
+    if (res != l_false) {        
+        TRACE("doc",
+              tout << mk_pp(fml1, m) << "\n";
+              tout << mk_pp(fml2, m) << "\n";
+              );
+        UNREACHABLE();
+        throw 0;
+    }
+    SASSERT(res == l_false);
+}
+
+expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
+    expr_ref result(m);
+    expr_ref_vector conj(m);
+    conj.push_back(tbvm().to_formula(m, src.pos()));
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i])));
+    }
+    result = mk_and(m, conj.size(), conj.c_ptr());
+    return result;
+}
+    
+void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
+    ast_manager& m = fml.get_manager();
+    expr_ref tmp1(m), tmp2(m);
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        if (to_delete[i]) {
+            expr_safe_replace rep1(m), rep2(m);
+            rep1.insert(tbvm().mk_var(m, i), m.mk_true());
+            rep1(fml, tmp1);
+            rep2.insert(tbvm().mk_var(m, i), m.mk_false());
+            rep2(fml, tmp2);
+            if (tmp1 == tmp2) {
+                fml = tmp1;
+            }
+            else {
+                fml = m.mk_or(tmp1, tmp2);
+            }
+        }
+    }
+}
+
+void doc_manager::project_rename(expr_ref& fml, bool const* to_delete) {
+    ast_manager& m = fml.get_manager();
+    expr_safe_replace rep(m);
+    for (unsigned i = 0, j = 0; i < num_tbits(); ++i) {
+        if (!to_delete[i]) {
+            rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i));
+            ++j;
+        }
+    }
+    rep(fml);
+}
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index 30858bbbd..86849ba72 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -87,10 +87,15 @@ public:
     bool well_formed(doc const& d) const;
     bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
     void set(doc& d, unsigned idx, tbit value);
+
+    void verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst);
 private:
     unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
     bool merge(doc& d, unsigned idx, subset_ints const& equalities, bit_vector const& discard_cols);
-    bool can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg);
+    void project_rename(expr_ref& fml, bool const* to_delete);
+    void project_expand(expr_ref& fml, bool const* to_delete);
+    expr_ref to_formula(ast_manager& m, doc const& src);
+    void check_equiv(ast_manager& m, expr* fml1, expr* fml2);
 };
 
 
@@ -185,7 +190,7 @@ public:
     }
     void insert(M& m, union_bvec const& other) {
         for (unsigned i = 0; i < other.size(); ++i) {
-            insert(m, other[i]);
+            insert(m, &other[i]);
         }
     }
     void intersect(M& m, union_bvec const& other) {
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 13aecbe09..371e14353 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -21,6 +21,7 @@ Revision History:
 
 
 #include"rel_context.h"
+#include"stopwatch.h"
 #include"dl_context.h"
 #include"dl_compiler.h"
 #include"dl_instruction.h"
@@ -97,7 +98,8 @@ namespace datalog {
           m_rmanager(ctx),
           m_answer(m), 
           m_last_result_relation(0),
-          m_ectx(ctx) {
+          m_ectx(ctx),
+          m_sw(0) {
 
         // register plugins for builtin tables
 
@@ -162,6 +164,9 @@ namespace datalog {
                 exit(0);
             }
 
+            ::stopwatch sw;
+            sw.start();
+
             compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
 
             TRACE("dl", m_code.display(*this, tout); );
@@ -180,6 +185,9 @@ namespace datalog {
             VERIFY( termination_code.perform(m_ectx) || m_context.canceled());
 
             m_code.process_all_costs();
+            sw.stop();
+            m_sw += sw.get_seconds();
+
 
             IF_VERBOSE(10, m_ectx.report_big_relations(1000, verbose_stream()););
 
@@ -562,6 +570,8 @@ namespace datalog {
     }
 
     void rel_context::collect_statistics(statistics& st) const {
+        st.update("saturation time", m_sw);
+        m_code.collect_statistics(st);
         m_ectx.collect_statistics(st);
     }
 
diff --git a/src/muz/rel/rel_context.h b/src/muz/rel/rel_context.h
index 5e26718d6..8cdee2766 100644
--- a/src/muz/rel/rel_context.h
+++ b/src/muz/rel/rel_context.h
@@ -41,6 +41,7 @@ namespace datalog {
         fact_vector        m_table_facts;
         execution_context  m_ectx;
         instruction_block  m_code;
+        double             m_sw;
 
         class scoped_query;
 
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 23a96981d..391445215 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -20,6 +20,7 @@ Revision History:
 
 #include "tbv.h"
 #include "hashtable.h"
+#include "ast_util.h"
 
 
 static bool s_debug_alloc = false;
@@ -269,3 +270,26 @@ std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const {
     }
     return out;
 }
+
+expr_ref tbv_manager::to_formula(ast_manager& m, tbv const& src) {
+    expr_ref result(m);
+    expr_ref_vector conj(m);
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        switch (src[i]) {
+        case BIT_0:
+            conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort())));
+            break;
+        case BIT_1:
+            conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort()));
+            break;
+        default:
+            break;
+        }
+    }
+    result = mk_and(m, conj.size(), conj.c_ptr());
+    return result;
+}
+
+expr_ref tbv_manager::mk_var(ast_manager& m, unsigned i) {
+    return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m);
+}
diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
index e701efcbe..454cbae37 100644
--- a/src/muz/rel/tbv.h
+++ b/src/muz/rel/tbv.h
@@ -23,6 +23,7 @@ Revision History:
 
 #include "fixed_bit_vector.h"
 #include "rational.h"
+#include "ast.h"
 
 class tbv;
 
@@ -80,6 +81,8 @@ public:
 
 
     static void debug_alloc();
+    expr_ref to_formula(ast_manager& m, tbv const& src);
+    expr_ref mk_var(ast_manager& m, unsigned i);
 };
 
 class tbv: private fixed_bit_vector {
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index fd3bf1415..b5af52701 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -2,6 +2,8 @@
 #include "dl_relation_manager.h"
 #include "qe_util.h"
 #include "ast_util.h"
+#include "smt_kernel.h"
+
 
 namespace datalog {
 
@@ -292,13 +294,17 @@ namespace datalog {
         doc_manager& dm;
         doc_manager& dm1;
         doc_manager& dm2;
+        unsigned_vector m_orig_cols1;
+        unsigned_vector m_orig_cols2;
     public:
         join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt,
                 const unsigned * cols1, const unsigned * cols2) 
             : convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2),
               dm(p.dm(get_result_signature())),
               dm1(t1.get_dm()),
-              dm2(t2.get_dm()) {
+              dm2(t2.get_dm()),
+              m_orig_cols1(m_cols1),
+              m_orig_cols2(m_cols2) {
             t1.expand_column_vector(m_cols1);
             t2.expand_column_vector(m_cols2);
         }
@@ -396,9 +402,12 @@ namespace datalog {
             TRACE("doc", result->display(tout << "result:\n"););
             IF_VERBOSE(3, result->display(verbose_stream() << "join result:\n"););
             SASSERT(r.well_formed(result->get_dm()));
+            DEBUG_CODE(p.verify_join(r1, r2, *result, m_orig_cols1.size(), m_orig_cols1.c_ptr(), m_orig_cols2.c_ptr()););
             return result;
         }
     };
+    
+
     relation_join_fn * udoc_plugin::mk_join_fn(
         const relation_base & t1, const relation_base & t2,
         unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
@@ -407,6 +416,7 @@ namespace datalog {
         }
         return alloc(join_fn, *this, get(t1), get(t2), col_cnt, cols1, cols2);
     }
+
     class udoc_plugin::project_fn : public convenient_relation_project_fn {
         svector<bool> m_to_delete;
     public:
@@ -550,6 +560,9 @@ namespace datalog {
             udoc_relation const& src = get(_src);
             udoc_relation* d = get(_delta);
             doc_manager& dm = r.get_dm();
+            ast_manager& m = r.get_plugin().get_ast_manager();
+            expr_ref fml0(m);
+            DEBUG_CODE(r.to_formula(fml0););
             udoc* d1 = 0;
             if (d) d1 = &d->get_udoc();
             if (d1) d1->reset(dm);
@@ -557,7 +570,9 @@ namespace datalog {
             SASSERT(r.get_udoc().well_formed(dm));
             SASSERT(!d1 || d1->well_formed(dm));
             TRACE("doc", _r.display(tout << "dst':\n"); );
-            IF_VERBOSE(3, _r.display(verbose_stream() << "union result:\n"););
+            IF_VERBOSE(3, r.display(verbose_stream() << "union: "););
+            IF_VERBOSE(3, if (d) d->display(verbose_stream() << "delta: "););
+            DEBUG_CODE(r.get_plugin().verify_union(fml0, src, r, d););
         }
     };
     void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) {
@@ -907,7 +922,8 @@ namespace datalog {
     class udoc_plugin::filter_interpreted_fn : public relation_mutator_fn {
         union_find_default_ctx union_ctx;
         doc_manager& dm;
-        expr_ref     m_condition;
+        expr_ref     m_original_condition;
+        expr_ref     m_reduced_condition;
         udoc         m_udoc;
         bit_vector   m_empty_bv;
         subset_ints  m_equalities;
@@ -915,7 +931,8 @@ namespace datalog {
     public:
         filter_interpreted_fn(const udoc_relation & t, ast_manager& m, app *condition) :
             dm(t.get_dm()),
-            m_condition(m),
+            m_original_condition(condition, m),
+            m_reduced_condition(m),            
             m_equalities(union_ctx) {
             unsigned num_bits = t.get_num_bits();
             m_empty_bv.resize(num_bits, false);
@@ -923,12 +940,12 @@ namespace datalog {
             for (unsigned i = 0; i < num_bits; ++i) {
                 m_equalities.mk_var();
             }        
-            t.extract_guard(condition, guard, m_condition);            
+            t.extract_guard(condition, guard, m_reduced_condition);            
             t.compile_guard(guard, m_udoc, m_empty_bv);
 
             TRACE("doc", 
                   tout << "original condition: " << mk_pp(condition, m) << "\n";
-                  tout << "remaining condition: " << m_condition << "\n"; 
+                  tout << "remaining condition: " << m_reduced_condition << "\n"; 
                   m_udoc.display(dm, tout) << "\n";);
         }
 
@@ -936,18 +953,22 @@ namespace datalog {
             m_udoc.reset(dm);
         }
         
-        virtual void operator()(relation_base & tb) {
+        virtual void operator()(relation_base & tb) {            
             udoc_relation & t = get(tb);
             udoc& u = t.get_udoc();
-            ast_manager& m = m_condition.get_manager();
+            ast_manager& m = m_reduced_condition.get_manager();
+            expr_ref fml0(m);
+            DEBUG_CODE(t.to_formula(fml0););
             SASSERT(u.well_formed(dm));
             u.intersect(dm, m_udoc);
             SASSERT(u.well_formed(dm));
-            t.apply_guard(m_condition, u, m_equalities, m_empty_bv);
+            t.apply_guard(m_reduced_condition, u, m_equalities, m_empty_bv);
             SASSERT(u.well_formed(dm));            
             u.simplify(dm);
             SASSERT(u.well_formed(dm));
             TRACE("doc", tout << "final size: " << t.get_size_estimate_rows() << '\n';);
+            IF_VERBOSE(3, t.display(verbose_stream()););
+            DEBUG_CODE(t.get_plugin().verify_filter(fml0, t, m_original_condition););
         }
     };
     relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) {
@@ -1048,7 +1069,8 @@ namespace datalog {
     class udoc_plugin::filter_proj_fn : public convenient_relation_project_fn {
         union_find_default_ctx union_ctx;
         doc_manager& dm;
-        expr_ref     m_condition;
+        expr_ref     m_original_condition;
+        expr_ref     m_reduced_condition;
         udoc         m_udoc;
         bit_vector   m_col_list; // map: col idx -> bool (whether the column is to be removed)
         svector<bool> m_to_delete; // same
@@ -1060,7 +1082,8 @@ namespace datalog {
                        unsigned col_cnt, const unsigned * removed_cols) :
             convenient_relation_project_fn(t.get_signature(), col_cnt, removed_cols),
             dm(t.get_dm()),
-            m_condition(m),
+            m_original_condition(condition, m),
+            m_reduced_condition(m),
             m_equalities(union_ctx) {
             t.expand_column_vector(m_removed_cols);
             unsigned num_bits = t.get_num_bits();
@@ -1075,9 +1098,9 @@ namespace datalog {
             for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
                 m_to_delete[m_removed_cols[i]] = true;
             }
-            expr_ref guard(m), non_eq_cond(m);
+            expr_ref guard(m), non_eq_cond(condition, m);
             t.extract_equalities(condition, non_eq_cond, m_equalities, m_roots);
-            t.extract_guard(non_eq_cond, guard, m_condition);            
+            t.extract_guard(non_eq_cond, guard, m_reduced_condition);            
             t.compile_guard(guard, m_udoc, m_col_list);
         }
         
@@ -1088,26 +1111,31 @@ namespace datalog {
             udoc_relation const & t = get(tb);
             udoc const& u1 = t.get_udoc();
             doc_manager& dm = t.get_dm();
-            ast_manager& m = m_condition.get_manager();
+            ast_manager& m = m_reduced_condition.get_manager();
             udoc  u2;
-            SASSERT(u1.well_formed(dm));
             u2.copy(dm, u1);
-            SASSERT(u2.well_formed(dm));
             u2.intersect(dm, m_udoc);
-            SASSERT(u2.well_formed(dm));
             u2.merge(dm, m_roots, m_equalities, m_col_list);
-            SASSERT(u2.well_formed(dm)); 
-            t.apply_guard(m_condition, u2, m_equalities, m_col_list);
-            SASSERT(u2.well_formed(dm));            
+            t.apply_guard(m_reduced_condition, u2, m_equalities, m_col_list);
+            SASSERT(u2.well_formed(dm));  
+            DEBUG_CODE(
+                expr_ref fml0(m);            
+                udoc_relation* r_test = get(t.get_plugin().mk_empty(t.get_signature()));
+                r_test->get_udoc().insert(dm, u2);
+                t.to_formula(fml0);
+                t.get_plugin().verify_filter(fml0, *r_test, m_original_condition);
+                r_test->deallocate(););
             udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
             doc_manager& dm2 = r->get_dm();
+            // std::cout << "Size of union: " << u2.size() << "\n";
             for (unsigned i = 0; i < u2.size(); ++i) {
                 doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), u2[i]);
+                dm.verify_project(m, dm2, m_to_delete.c_ptr(), u2[i], *d);
                 r->get_udoc().insert(dm2, d);
                 SASSERT(r->get_udoc().well_formed(dm2));
             }
             u2.reset(dm);
-            IF_VERBOSE(3, r->display(verbose_stream() << "filter result:\n"););
+            IF_VERBOSE(3, r->display(verbose_stream() << "filter project result:\n"););
             return r;
         }
     };
@@ -1117,5 +1145,113 @@ namespace datalog {
         return check_kind(t)?alloc(filter_proj_fn, get(t), get_ast_manager(), condition, removed_col_cnt, removed_cols):0;
     }
 
+    // TBD: move this to relation validation module like table_checker.
+    void udoc_plugin::verify_join(relation_base const& t1, relation_base const& t2, relation_base const& t,
+                                  unsigned sz, unsigned const* cols1, unsigned const* cols2) {
+        ast_manager& m = get_ast_manager();
+        expr_ref fml1(m), fml2(m), fml3(m);
+        
+        relation_signature const& sig1 = t1.get_signature();
+        relation_signature const& sig2 = t2.get_signature();
+        relation_signature const& sig  = t.get_signature();
+        var_ref var1(m), var2(m);
+        t1.to_formula(fml1);
+        t2.to_formula(fml2);
+        t.to_formula(fml3);
+        var_subst sub(m, false);
+        expr_ref_vector vars(m);
+        for (unsigned i = 0; i < sig2.size(); ++i) {
+            vars.push_back(m.mk_var(i + sig1.size(), sig2[i]));
+        }
+        sub(fml2, vars.size(), vars.c_ptr(), fml2);
+        fml1 = m.mk_and(fml1, fml2);
+        for (unsigned i = 0; i < sz; ++i) {
+            unsigned v1 = cols1[i];
+            unsigned v2 = cols2[i];
+            var1 = m.mk_var(v1, sig1[v1]);
+            var2 = m.mk_var(v2 + sig1.size(), sig2[v2]);
+            fml1 = m.mk_and(m.mk_eq(var1, var2), fml1);
+        }
+        vars.reset();
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            std::stringstream strm;
+            strm << "x" << i;
+            vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));            
+        }
+        sub(fml1, vars.size(), vars.c_ptr(), fml1);
+        sub(fml3, vars.size(), vars.c_ptr(), fml3);
+        check_equiv(fml1, fml3);
+    }
+
+    void udoc_plugin::verify_filter(expr* fml0, relation_base const& t, expr* cond) {
+        expr_ref fml1(m), fml2(m);
+        fml1 = m.mk_and(fml0, cond);
+        t.to_formula(fml2);
+        
+        relation_signature const& sig = t.get_signature();
+        expr_ref_vector vars(m);
+        var_subst sub(m, false);
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            std::stringstream strm;
+            strm << "x" << i;
+            vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));            
+        }
+        sub(fml1, vars.size(), vars.c_ptr(), fml1);
+        sub(fml2, vars.size(), vars.c_ptr(), fml2);
+        check_equiv(fml1, fml2);
+    }
+
+    void udoc_plugin::check_equiv(expr* fml1, expr* fml2) {
+        TRACE("doc", tout << mk_pp(fml1, m) << "\n";
+              tout << mk_pp(fml2, m) << "\n";);
+        smt_params fp;
+        smt::kernel solver(m, fp);
+        expr_ref tmp(m);
+        tmp = m.mk_not(m.mk_eq(fml1, fml2));
+        solver.assert_expr(tmp);
+        lbool res = solver.check();
+        IF_VERBOSE(3, verbose_stream() << "result of verification: " << res << "\n";);
+        if (res != l_false) {
+            throw 0;
+        }
+        SASSERT(res == l_false);            
+    }
+
+    void udoc_plugin::verify_union(expr* fml0, relation_base const& src, relation_base const& dst, relation_base const* delta) {
+        expr_ref fml1(m), fml2(m), fml3(m);
+        src.to_formula(fml1);
+        dst.to_formula(fml2);
+        fml1 = m.mk_or(fml1, fml0);
+        relation_signature const& sig = dst.get_signature();
+        expr_ref_vector vars(m);
+        var_subst sub(m, false);
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            std::stringstream strm;
+            strm << "x" << i;
+            vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));            
+        }
+        sub(fml1, vars.size(), vars.c_ptr(), fml1);
+        sub(fml2, vars.size(), vars.c_ptr(), fml2);
+
+        check_equiv(fml1, fml2);
+
+        if (delta) {
+            delta->to_formula(fml3);
+            // dst >= delta >= dst \ fml0
+            // dst \ fml0 == delta & dst & \ fml0
+            // dst & delta = delta
+            expr_ref fml4(m), fml5(m);
+            fml4 = m.mk_and(fml2, m.mk_not(fml0));
+            fml5 = m.mk_and(fml3, fml4);
+            sub(fml4, vars.size(), vars.c_ptr(), fml4);
+            sub(fml5, vars.size(), vars.c_ptr(), fml5);
+            check_equiv(fml4, fml5);
+            fml4 = m.mk_and(fml3, fml2);
+            sub(fml3, vars.size(), vars.c_ptr(), fml3);
+            sub(fml4, vars.size(), vars.c_ptr(), fml4);
+            check_equiv(fml3, fml4);
+        }
+    }
+
 
 }
diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h
index 64ced8e83..6b7a218b5 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/src/muz/rel/udoc_relation.h
@@ -133,6 +133,15 @@ namespace datalog {
         virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn(
             const relation_base & t, app * condition,
             unsigned removed_col_cnt, const unsigned * removed_cols);
+
+        void verify_join(relation_base const& t1, relation_base const& t2, relation_base const& t,
+                         unsigned sz, unsigned const* cols1, unsigned const* cols2);
+
+        void verify_filter(expr* fml0, relation_base const& t, expr* cond);
+
+        void verify_union(expr* fml0, relation_base const& src, relation_base const& dst, relation_base const* delta);
+
+        void check_equiv(expr* f1, expr* f2);
     };
 };
        
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index 2921f52c9..ad62893d8 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -261,7 +261,12 @@ class test_doc_cls {
                 rep1(fml, tmp1);
                 rep2.insert(m_vars[i].get(), m.mk_false());
                 rep2(fml, tmp2);
-                fml = m.mk_or(tmp1, tmp2);
+                if (tmp1 == tmp2) {
+                    fml1 = tmp1;
+                }
+                else {
+                    fml = m.mk_or(tmp1, tmp2);
+                }
             }
         }
     }
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index dbe8d9b83..5c25c8ee7 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -443,7 +443,7 @@ public:
         join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr());
         t = (*join_fn)(*t1, *t2);
 
-        verify_join(*t1, *t2, *t, jc1.size(), jc1.c_ptr(), jc2.c_ptr());
+        p.verify_join(*t1, *t2, *t, jc1.size(), jc1.c_ptr(), jc2.c_ptr());
         t1->display(std::cout);
         t2->display(std::cout);
         t->display(std::cout);
@@ -459,43 +459,6 @@ public:
         return t;
     }
 
-    void verify_join(relation_base const& t1, relation_base& t2, relation_base& t,
-                     unsigned sz, unsigned const* cols1, unsigned const* cols2) {
-        relation_signature const& sig1 = t1.get_signature();
-        relation_signature const& sig2 = t2.get_signature();
-        relation_signature const& sig  = t.get_signature();
-        expr_ref fml1(m), fml2(m), fml3(m);
-        var_ref var1(m), var2(m);
-        t1.to_formula(fml1);
-        t2.to_formula(fml2);
-        t.to_formula(fml3);
-        var_subst sub(m, false);
-        expr_ref_vector vars(m);
-        for (unsigned i = 0; i < sig2.size(); ++i) {
-            vars.push_back(m.mk_var(i + sig1.size(), sig2[i]));
-        }
-        sub(fml2, vars.size(), vars.c_ptr(), fml2);
-        fml1 = m.mk_and(fml1, fml2);
-        for (unsigned i = 0; i < sz; ++i) {
-            unsigned v1 = cols1[i];
-            unsigned v2 = cols2[i];
-            var1 = m.mk_var(v1, sig1[v1]);
-            var2 = m.mk_var(v2 + sig1.size(), sig2[v2]);
-            fml1 = m.mk_and(m.mk_eq(var1, var2), fml1);
-        }
-        vars.reset();
-        for (unsigned i = 0; i < sig.size(); ++i) {
-            std::stringstream strm;
-            strm << "x" << i;
-            vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));            
-        }
-        sub(fml1, vars.size(), vars.c_ptr(), fml1);
-        sub(fml3, vars.size(), vars.c_ptr(), fml3);
-        check_equiv(fml1, fml3);
-    }
-    
-    
-
     void check_permutation(relation_base* t1, unsigned_vector const& cycle) {
         scoped_ptr<datalog::relation_transformer_fn> rename;
         rename = p.mk_rename_fn(*t1, cycle.size(), cycle.c_ptr());        
@@ -739,41 +702,16 @@ public:
         udoc_relation* full = mk_full(t.get_signature());
         rel_union union_fn = p.mk_union_fn(t, *full, 0);
         (*union_fn)(t, *full, 0);
+        expr_ref fml0(m);
+        t.to_formula(fml0);
         rel_mut fint = p.mk_filter_interpreted_fn(t, cond);
         (*fint)(t);
         t.display(std::cout << "filter: " << mk_pp(cond, m) << " "); std::cout << "\n";
-        verify_filter(t, cond);
+        t.get_plugin().verify_filter(fml0, t, cond);
         full->deallocate();
     }
 
-    void verify_filter(udoc_relation& r, expr* fml2) {
-        expr_ref fml1(m), tmp(m);
-        r.to_formula(fml1);
-        tmp = m.mk_not(m.mk_eq(fml1, fml2));
-        relation_signature const& sig = r.get_signature();
-        expr_ref_vector vars(m);
-        var_subst sub(m, false);
-        for (unsigned i = 0; i < sig.size(); ++i) {
-            std::stringstream strm;
-            strm << "x" << i;
-            vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));            
-        }
 
-        sub(tmp, vars.size(), vars.c_ptr(), tmp);
-        
-        smt_params fp;
-        smt::kernel solver(m, fp);
-        TRACE("doc", 
-              tout << "Original formula:\n";
-              tout << mk_pp(fml2, m) << "\n";
-              tout << "Filtered formula: \n";
-              tout << mk_pp(fml1,m) << "\n";
-              tout << tmp << "\n";
-              );
-        solver.assert_expr(tmp);
-        lbool res = solver.check();
-        SASSERT(res == l_false);
-    }
 };
 
 void tst_udoc_relation() {
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index 661d3762b..b0edc2626 100644
--- a/src/util/stopwatch.h
+++ b/src/util/stopwatch.h
@@ -69,6 +69,7 @@ public:
 #undef ARRAYSIZE
 #define ARRAYSIZE ARRAYSIZE_TEMP
 #undef max
+#undef min
 
 
 #elif defined(__APPLE__) && defined (__MACH__) // Mac OS X