diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 9e8789aa6..05135a44f 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -278,7 +278,9 @@ namespace datalog {
     bool context::use_map_names() const { return m_params->datalog_use_map_names(); }
     bool context::fix_unbound_vars() const { return m_params->xform_fix_unbound_vars(); }
     symbol context::default_table() const { return m_params->datalog_default_table(); }
-    symbol context::default_relation() const { return m_params->datalog_default_relation(); } // external_relation_plugin::get_name()); 
+    symbol context::default_relation() const { return m_default_relation; }
+    void context::set_default_relation(symbol const& s) { m_default_relation = s; }
+    symbol context::check_relation() const { return m_params->datalog_check_relation(); }
     symbol context::default_table_checker() const { return m_params->datalog_default_table_checker(); }
     bool context::default_table_checked() const { return m_params->datalog_default_table_checked(); }
     bool context::dbg_fpr_nonempty_relation_signature() const { return m_params->datalog_dbg_fpr_nonempty_relation_signature(); }
@@ -840,6 +842,7 @@ namespace datalog {
         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(); 
+        m_default_relation = m_params->datalog_default_relation(); 
     }
 
     expr_ref context::get_background_assertion() {
@@ -1005,6 +1008,7 @@ namespace datalog {
     void context::ensure_engine() {
         if (!m_engine.get()) {
             m_engine = m_register_engine.mk_engine(get_engine());
+            m_engine->updt_params();
 
             // break abstraction.
             if (get_engine() == DATALOG_ENGINE) {
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 0b9c623c4..67520d94f 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -173,6 +173,7 @@ namespace datalog {
         fixedpoint_params*  m_params;
         bool               m_generate_proof_trace;
         bool               m_unbound_compressor;
+        symbol             m_default_relation;
         dl_decl_util       m_decl_util;
         th_rewriter        m_rewriter;
         var_subst          m_var_subst;
@@ -250,7 +251,9 @@ namespace datalog {
         bool fix_unbound_vars() const;
         symbol default_table() const;
         symbol default_relation() const;
-        symbol default_table_checker() const;
+        void set_default_relation(symbol const& s);
+        symbol default_table_checker() const;        
+        symbol check_relation() const;
         bool default_table_checked() const;
         bool dbg_fpr_nonempty_relation_signature() const;
         unsigned dl_profile_milliseconds_threshold() const;
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 7951a62bc..3e31c9e48 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -37,6 +37,8 @@ def_module_params('fixedpoint',
                            'table will be default_table inside a wrapper that checks that its results ' +
                            'are the same as of default_table_checker table'),
                           ('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"),
+                          ('datalog.check_relation',SYMBOL,'null', "name of default relation to check. " +
+                           "operations on the default relation will be verified using SMT solving"),
                           ('datalog.initial_restart_timeout', UINT, 0, 
                            "length of saturation run before the first restart (in ms), " + 
                            "zero means no restarts"),
diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp
new file mode 100644
index 000000000..beafc7c3e
--- /dev/null
+++ b/src/muz/rel/check_relation.cpp
@@ -0,0 +1,641 @@
+#include "check_relation.h"
+#include "dl_relation_manager.h"
+#include "qe_util.h"
+#include "ast_util.h"
+#include "smt_kernel.h"
+
+
+namespace datalog {
+
+    check_relation::check_relation(check_relation_plugin& p, relation_signature const& sig, relation_base* r):
+        relation_base(p, sig),
+        m(p.get_ast_manager()),
+        m_relation(r),
+        m_fml(m) {
+        m_relation->to_formula(m_fml);
+    }
+    check_relation::~check_relation() {
+        m_relation->deallocate();
+    }
+    void check_relation::check_equiv(expr* f1, expr* f2) const { 
+        get_plugin().check_equiv(f1, f2); 
+    }
+    void check_relation::consistent_formula() {
+        expr_ref fml(m);
+        m_relation->to_formula(fml);
+        if (m_fml != fml) {
+            IF_VERBOSE(0, display(verbose_stream() << "relation does not have a consistent formula"););
+        }
+    }
+    expr_ref check_relation::mk_eq(relation_fact const& f) const {
+        relation_signature const& sig = get_signature();
+        expr_ref_vector conjs(m);
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), f[i]));
+        }
+        return expr_ref(mk_and(m, conjs.size(), conjs.c_ptr()), m);
+    }
+
+    expr_ref check_relation::ground(expr* fml) const {
+        relation_signature const& sig = get_signature();
+        var_subst sub(m, false);
+        expr_ref_vector vars(m);
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            vars.push_back(m.mk_const(symbol(i), sig[i]));
+        }
+        expr_ref result(m);
+        sub(fml, vars.size(), vars.c_ptr(), result);
+        return result;
+    }
+
+    void check_relation::add_fact(const relation_fact & f) {
+        expr_ref fml1(m);
+        m_relation->add_fact(f);
+        m_relation->to_formula(fml1);
+        m_fml = m.mk_or(m_fml, mk_eq(f));        
+        check_equiv(ground(m_fml), ground(fml1));
+        m_fml = fml1;
+    }
+    void check_relation::add_new_fact(const relation_fact & f) {
+        expr_ref fml1(m);
+        m_relation->add_new_fact(f);
+        m_relation->to_formula(fml1);
+        m_fml = m.mk_or(m_fml, mk_eq(f));
+        check_equiv(ground(m_fml), ground(fml1));
+        m_fml = fml1;
+    }
+    bool check_relation::empty() const {
+        bool result = m_relation->empty();
+        if (result && !m.is_false(m_fml)) {
+            check_equiv(m.mk_false(), ground(m_fml));
+        }
+        return result;
+    }
+    bool check_relation::fast_empty() const {
+        bool result = m_relation->fast_empty();
+        if (result && !m.is_false(m_fml)) {
+            check_equiv(m.mk_false(), ground(m_fml));
+        }
+        return result;
+    }
+    void check_relation::reset() {
+        m_relation->reset();
+        m_fml = m.mk_false();
+    }
+
+    bool check_relation::contains_fact(const relation_fact & f) const {
+        bool result = m_relation->contains_fact(f);
+        expr_ref fml1(m), fml2(m);
+        fml1 = mk_eq(f);
+        fml2 = m.mk_and(m_fml, fml1);
+        if (result) {
+            check_equiv(ground(fml1), ground(fml2));            
+        }
+        else if (!m.is_false(m_fml)) {
+            check_equiv(ground(fml2), m.mk_false());            
+        }
+        return result;
+    }
+    check_relation * check_relation::clone() const {
+        check_relation* result = check_relation_plugin::get(get_plugin().mk_empty(get_signature()));
+        result->m_relation->deallocate();
+        result->m_relation = m_relation->clone();
+        result->m_relation->to_formula(result->m_fml);
+        if (m_fml != result->m_fml) {
+            check_equiv(ground(m_fml), ground(result->m_fml));
+        }
+        return result;
+    }
+    check_relation * check_relation::complement(func_decl* f) const {
+        check_relation* result = check_relation_plugin::get(get_plugin().mk_empty(get_signature()));
+        result->m_relation->deallocate();
+        result->m_relation = m_relation->complement(f);
+        result->m_relation->to_formula(result->m_fml);
+        expr_ref fml(m);
+        fml = m.mk_not(m_fml);
+        check_equiv(ground(fml), ground(result->m_fml));
+        return result;
+    }
+    void check_relation::to_formula(expr_ref& fml) const {
+        fml = m_fml;
+    }
+
+    check_relation_plugin& check_relation::get_plugin() const {
+        return static_cast<check_relation_plugin&>(relation_base::get_plugin());
+    }
+
+    void check_relation::display(std::ostream& out) const {
+        m_relation->display(out);
+        out << m_fml << "\n";
+    }
+
+    // -------------
+
+    check_relation_plugin::check_relation_plugin(relation_manager& rm):
+        relation_plugin(check_relation_plugin::get_name(), rm),
+        m(rm.get_context().get_manager()),
+        m_base(0) {
+    }
+    check_relation_plugin::~check_relation_plugin() {
+    }
+    check_relation& check_relation_plugin::get(relation_base& r) {
+        return dynamic_cast<check_relation&>(r);
+    }
+    check_relation* check_relation_plugin::get(relation_base* r) {
+        return r?dynamic_cast<check_relation*>(r):0;
+    }
+    check_relation const & check_relation_plugin::get(relation_base const& r) {
+        return dynamic_cast<check_relation const&>(r);        
+    }
+
+    bool check_relation_plugin::can_handle_signature(const relation_signature & sig) {
+        return m_base->can_handle_signature(sig);
+    }
+    relation_base * check_relation_plugin::mk_empty(const relation_signature & sig) {
+        relation_base* r = m_base->mk_empty(sig);
+        return alloc(check_relation, *this, sig, r);
+    }
+    relation_base * check_relation_plugin::mk_full(func_decl* p, const relation_signature & s) {
+        relation_base* r = m_base->mk_full(p, s);
+        return alloc(check_relation, *this, s, r);
+    }
+
+    class check_relation_plugin::join_fn : public convenient_relation_join_fn {
+        scoped_ptr<relation_join_fn> m_join;
+    public:
+        join_fn(relation_join_fn* j,
+                 const relation_signature & o1_sig, const relation_signature & o2_sig, unsigned col_cnt,
+                 const unsigned * cols1, const unsigned * cols2)
+            : convenient_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2), m_join(j) 
+        {}
+        virtual ~join_fn() {}
+        virtual relation_base * operator()(const relation_base & r1, const relation_base & r2) {
+            check_relation const& t1 = get(r1);
+            check_relation const& t2 = get(r2);
+            check_relation_plugin& p = t1.get_plugin();
+            relation_base* r = (*m_join)(t1.rb(), t2.rb());
+            p.verify_join(r1, r2, *r, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr());
+            return alloc(check_relation, p, r->get_signature(), r);
+        }
+    };    
+
+    relation_join_fn * check_relation_plugin::mk_join_fn(
+        const relation_base & t1, const relation_base & t2,
+        unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {        
+        relation_join_fn* j = m_base->mk_join_fn(get(t1).rb(), get(t2).rb(), col_cnt, cols1, cols2);
+        return j?alloc(join_fn, j, t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2):0;        
+    }
+
+    void check_relation_plugin::verify_filter_project(
+        relation_base const& src, relation_base const& dst, 
+        app* cond, unsigned_vector const& removed_cols) {
+        expr_ref fml1(m), fml2(m);
+        src.to_formula(fml1);
+        dst.to_formula(fml2);
+        fml1 = m.mk_and(cond, fml1);
+        verify_project(src, fml1, dst, fml2, removed_cols);
+    }
+
+    void check_relation_plugin::verify_project(
+        relation_base const& src, 
+        relation_base const& dst, 
+        unsigned_vector const& removed_cols) {
+        expr_ref fml1(m), fml2(m);
+        src.to_formula(fml1);
+        dst.to_formula(fml2);
+        verify_project(src, fml1, dst, fml2, removed_cols);
+    }
+    void check_relation_plugin::verify_project(
+        relation_base const& src, expr* f1, 
+        relation_base const& dst, expr* f2,
+        unsigned_vector const& removed_cols) {
+        expr_ref fml1(m);
+        expr_ref fml2(m);
+        expr_ref_vector vars1(m), vars2(m);
+        ptr_vector<sort> bound;
+        svector<symbol> names;
+        relation_signature const& sig1 = src.get_signature();
+        relation_signature const& sig2 = dst.get_signature();
+        for (unsigned i = 0; i < sig2.size(); ++i) {
+            vars2.push_back(m.mk_const(symbol(i), sig2[i]));
+        }
+        for (unsigned i = 0, j = 0, k = 0; i < sig1.size(); ++i) {
+            if (j < removed_cols.size() && removed_cols[j] == i) {
+                std::ostringstream strm;
+                strm << "x" << j;
+                bound.push_back(sig1[i]);                
+                names.push_back(symbol(strm.str().c_str()));
+                vars1.push_back(m.mk_var(j, sig1[i]));
+                ++j;
+            }
+            else {
+                vars1.push_back(vars2[k].get());
+                SASSERT(m.get_sort(vars2[k].get()) == sig1[i]);
+                ++k;
+            }
+        }
+        var_subst sub(m, false);
+        sub(f1, vars1.size(), vars1.c_ptr(), fml1);
+        sub(f2, vars2.size(), vars2.c_ptr(), fml2);
+        bound.reverse();        
+        fml1 = m.mk_exists(bound.size(), bound.c_ptr(), names.c_ptr(), fml1);
+        check_equiv(fml1, fml2);
+    }
+
+    void check_relation_plugin::verify_permutation(
+        relation_base const& src, relation_base const& dst, 
+        unsigned_vector const& cycle) {
+        unsigned_vector perm;
+        relation_signature const& sig1 = src.get_signature();
+        relation_signature const& sig2 = dst.get_signature();
+        for (unsigned i = 0; i < sig1.size(); ++i) {
+            perm.push_back(i);
+        }
+        for (unsigned i = 0; i < cycle.size(); ++i) {
+            unsigned j = (i + 1)%cycle.size();
+            unsigned col1 = cycle[i];
+            unsigned col2 = cycle[j];
+            perm[col2] = col1;
+        }
+        for (unsigned i = 0; i < perm.size(); ++i) {
+            SASSERT(sig2[perm[i]] == sig1[i]);
+        }
+        expr_ref_vector sub(m);
+        for (unsigned i = 0; i < perm.size(); ++i) {
+            sub.push_back(m.mk_var(perm[i], sig1[i]));
+        }
+        var_subst subst(m, false);
+        expr_ref fml1(m), fml2(m);
+        src.to_formula(fml1);
+        dst.to_formula(fml2);
+        subst(fml1, sub.size(), sub.c_ptr(), fml1);
+        expr_ref_vector vars(m);
+        for (unsigned i = 0; i < sig2.size(); ++i) {
+            vars.push_back(m.mk_const(symbol(i), sig2[i]));            
+        }
+
+        subst(fml1, vars.size(), vars.c_ptr(), fml1);
+        subst(fml2, vars.size(), vars.c_ptr(), fml2);
+        
+        check_equiv(fml1, fml2);
+    }
+
+    void check_relation_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 check_relation_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 check_relation_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 (res == l_false) {
+            IF_VERBOSE(3, verbose_stream() << "verified\n";);
+        }
+        else {
+            IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n";
+                       verbose_stream() << mk_pp(fml1, m) << "\n";
+                       verbose_stream() << mk_pp(fml2, m) << "\n";);
+            throw 0;
+        }
+    }
+
+    void check_relation_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);
+        }
+    }
+
+    class check_relation_plugin::union_fn : public relation_union_fn {
+        scoped_ptr<relation_union_fn> m_union;
+    public:
+        union_fn(relation_union_fn* m): m_union(m) {}
+
+        virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) {
+            TRACE("doc", _r.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
+            check_relation& r = get(_r);
+            check_relation const& src = get(_src);
+            check_relation* d = get(_delta);
+            expr_ref fml0 = r.m_fml;
+            (*m_union)(r.rb(), src.rb(), d?(&d->rb()):0);
+            r.get_plugin().verify_union(fml0, src.rb(), r.rb(), d?(&d->rb()):0);
+            r.rb().to_formula(r.m_fml);
+            if (d) d->rb().to_formula(d->m_fml);
+        }
+    };
+    relation_union_fn * check_relation_plugin::mk_union_fn(
+        const relation_base & tgt, const relation_base & src, 
+        const relation_base * delta) {
+        relation_base const* d1 = delta?(&(get(*delta).rb())):0;
+        relation_union_fn* u = m_base->mk_union_fn(get(tgt).rb(), get(src).rb(), d1);
+        return u?alloc(union_fn, u):0;
+    }
+    relation_union_fn * check_relation_plugin::mk_widen_fn(
+        const relation_base & tgt, const relation_base & src, 
+        const relation_base * delta) {
+        relation_base const* d1 = delta?(&(get(*delta).rb())):0;
+        relation_union_fn* u = m_base->mk_widen_fn(get(tgt).rb(), get(src).rb(), d1);
+        return u?alloc(union_fn, u):0;
+    }
+
+    class check_relation_plugin::filter_identical_fn : public relation_mutator_fn {        
+        unsigned_vector                 m_cols;
+        scoped_ptr<relation_mutator_fn> m_filter;
+    public:
+        filter_identical_fn(relation_mutator_fn* f, unsigned col_cnt, const unsigned *identical_cols)
+            : m_cols(col_cnt, identical_cols),
+              m_filter(f) {
+        }
+
+        virtual ~filter_identical_fn() {}
+        
+        virtual void operator()(relation_base & _r) {
+            check_relation& r = get(_r);
+            check_relation_plugin& p = r.get_plugin();            
+            ast_manager& m = p.m;
+            expr_ref cond(m);
+            relation_signature const& sig = r.get_signature();
+            expr_ref_vector conds(m);
+            unsigned c1 = m_cols[0];
+            for (unsigned i = 1; i < m_cols.size(); ++i) {
+                unsigned c2 = m_cols[i];
+                conds.push_back(m.mk_eq(m.mk_var(c1, sig[c1]), m.mk_var(c2, sig[c2])));
+            }
+            cond = mk_and(m, conds.size(), conds.c_ptr());
+            r.consistent_formula();
+            (*m_filter)(r.rb());
+            p.verify_filter(r.m_fml, r.rb(), cond);
+            r.rb().to_formula(r.m_fml);
+        }
+    };
+    relation_mutator_fn * check_relation_plugin::mk_filter_identical_fn(
+        const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) {
+        relation_mutator_fn* r = m_base->mk_filter_identical_fn(get(t).rb(), col_cnt, identical_cols);
+        return r?alloc(filter_identical_fn, r, col_cnt, identical_cols):0;
+    }
+
+    class check_relation_plugin::filter_interpreted_fn : public relation_mutator_fn {
+        scoped_ptr<relation_mutator_fn> m_mutator;
+        app_ref m_condition;
+    public:
+        filter_interpreted_fn(relation_mutator_fn* r, app_ref& condition) :
+            m_mutator(r),
+            m_condition(condition) {
+        }
+
+        virtual ~filter_interpreted_fn() {}
+        
+        virtual void operator()(relation_base & tb) {            
+            check_relation& r = get(tb);
+            check_relation_plugin& p = r.get_plugin();            
+            expr_ref fml = r.m_fml;
+            (*m_mutator)(r.rb());
+            p.verify_filter(fml, r.rb(), m_condition);
+            r.rb().to_formula(r.m_fml);
+        }
+    };
+    relation_mutator_fn * check_relation_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) {
+        relation_mutator_fn* r = m_base->mk_filter_interpreted_fn(get(t).rb(), condition);
+        app_ref cond(condition, m);
+        return r?alloc(filter_interpreted_fn, r, cond):0;
+    }
+
+    class check_relation_plugin::project_fn : public convenient_relation_project_fn {
+        scoped_ptr<relation_transformer_fn> m_project;
+    public:
+        project_fn(relation_transformer_fn* p,
+                   relation_base const & t, 
+                   unsigned removed_col_cnt, const unsigned * removed_cols) 
+            : convenient_relation_project_fn(t.get_signature(), removed_col_cnt, removed_cols),
+              m_project(p) {
+        }
+
+        virtual ~project_fn() {}
+
+        virtual relation_base * operator()(const relation_base & tb) {
+            check_relation const& t = get(tb);
+            check_relation_plugin& p = t.get_plugin();
+            relation_base* r = (*m_project)(t.rb());
+            p.verify_project(tb, *r, m_removed_cols);
+            return alloc(check_relation, p, r->get_signature(), r);
+        }
+    };
+    
+
+    relation_transformer_fn * check_relation_plugin::mk_project_fn(
+        const relation_base & t, unsigned col_cnt, 
+        const unsigned * removed_cols) {
+        relation_transformer_fn* p = m_base->mk_project_fn(get(t).rb(), col_cnt, removed_cols);
+        return p?alloc(project_fn, p, t, col_cnt, removed_cols):0;
+    }
+
+    class check_relation_plugin::rename_fn : public convenient_relation_rename_fn {
+        scoped_ptr<relation_transformer_fn> m_permute;
+    public:
+        rename_fn(relation_transformer_fn* permute, 
+                  relation_base const& t, unsigned cycle_len, const unsigned * cycle) 
+            : convenient_relation_rename_fn(t.get_signature(), cycle_len, cycle),
+              m_permute(permute) {
+        }
+
+        virtual ~rename_fn() {}
+
+        virtual relation_base * operator()(const relation_base & _t) {
+            check_relation const& t = get(_t);
+            check_relation_plugin& p = t.get_plugin();            
+            relation_signature const& sig = get_result_signature();
+            relation_base* r = (*m_permute)(t.rb());         
+            p.verify_permutation(t.rb(), *r, m_cycle);
+            return alloc(check_relation, p, sig, r);            
+        }
+    };
+    relation_transformer_fn * check_relation_plugin::mk_rename_fn(
+        const relation_base & r, 
+        unsigned cycle_len, const unsigned * permutation_cycle) {
+        relation_transformer_fn* p = m_base->mk_rename_fn(get(r).rb(), cycle_len, permutation_cycle);
+        return p?alloc(rename_fn, p, r, cycle_len, permutation_cycle):0;
+    }
+
+    class check_relation_plugin::filter_equal_fn : public relation_mutator_fn {
+        scoped_ptr<relation_mutator_fn> m_filter;
+        relation_element m_val;
+        unsigned         m_col;
+    public:
+        filter_equal_fn(relation_mutator_fn* filter, relation_base const& t, 
+                        const relation_element val, unsigned col):
+            m_filter(filter), 
+            m_val(val),
+            m_col(col)
+        {}
+        virtual ~filter_equal_fn() { }        
+        virtual void operator()(relation_base & tb) {
+            check_relation & t = get(tb);
+            check_relation_plugin& p = t.get_plugin();
+            (*m_filter)(t.rb());
+            expr_ref fml = t.m_fml;
+            t.rb().to_formula(t.m_fml);
+            fml = p.m.mk_and(fml, p.m.mk_eq(p.m.mk_var(m_col, t.get_signature()[m_col]), m_val));
+            p.check_equiv(t.ground(fml), t.ground(t.m_fml));
+        }
+    };
+    relation_mutator_fn * check_relation_plugin::mk_filter_equal_fn(
+        const relation_base & t, const relation_element & value, unsigned col) {
+        relation_mutator_fn* r = m_base->mk_filter_equal_fn(get(t).rb(), value, col);
+        return r?alloc(filter_equal_fn, r, t, value, col):0;
+    }
+
+
+
+
+    class check_relation_plugin::negation_filter_fn : public relation_intersection_filter_fn {
+        scoped_ptr<relation_intersection_filter_fn> m_filter;
+        const unsigned_vector m_t_cols;
+        const unsigned_vector m_neg_cols;
+    public:
+        negation_filter_fn(
+            relation_intersection_filter_fn* filter,
+            unsigned joined_col_cnt, const unsigned *t_cols, const unsigned *neg_cols)
+            : m_filter(filter), 
+              m_t_cols(joined_col_cnt, t_cols), m_neg_cols(joined_col_cnt, neg_cols) {
+            SASSERT(joined_col_cnt > 0);
+        }
+        
+        virtual void operator()(relation_base& tb, const relation_base& negb) {
+            check_relation& t = get(tb);
+            check_relation const& n = get(negb);
+            check_relation_plugin& p = t.get_plugin();
+            (*m_filter)(t.rb(), n.rb());
+            IF_VERBOSE(0, verbose_stream() << "TBD: verify filter_negation\n";);
+            t.rb().to_formula(t.m_fml);
+        }
+    };
+
+    relation_intersection_filter_fn * check_relation_plugin::mk_filter_by_negation_fn(
+        const relation_base& t,
+        const relation_base& neg, unsigned joined_col_cnt, const unsigned *t_cols,
+        const unsigned *negated_cols) {
+        relation_intersection_filter_fn* f = mk_filter_by_negation_fn(get(t).rb(), get(neg).rb(), joined_col_cnt, t_cols, negated_cols);
+        return f?alloc(negation_filter_fn, f, joined_col_cnt, t_cols, negated_cols):0;
+    }
+
+
+    class check_relation_plugin::filter_proj_fn : public convenient_relation_project_fn {
+        app_ref     m_cond;
+        scoped_ptr<relation_transformer_fn> m_xform;
+    public:
+        filter_proj_fn(relation_transformer_fn* xform,
+                       relation_base const& t, app_ref& cond,
+                       unsigned col_cnt, const unsigned * removed_cols) :
+            convenient_relation_project_fn(t.get_signature(), col_cnt, removed_cols),
+            m_cond(cond),
+            m_xform(xform)
+        {}
+        
+        virtual ~filter_proj_fn() {}
+
+        virtual relation_base* operator()(const relation_base & tb) {
+            check_relation const & t = get(tb);
+            check_relation_plugin& p = t.get_plugin();
+            relation_base* r = (*m_xform)(t.rb());
+            p.verify_filter_project(t.rb(), *r, m_cond, m_removed_cols);
+            relation_signature const& sig = get_result_signature();
+            return alloc(check_relation, p, sig, r);
+        }
+    };
+    relation_transformer_fn * check_relation_plugin::mk_filter_interpreted_and_project_fn(
+        const relation_base & t, app * condition,
+        unsigned removed_col_cnt, const unsigned * removed_cols) {
+        relation_transformer_fn* r = m_base->mk_filter_interpreted_and_project_fn(get(t).rb(), condition, removed_col_cnt, removed_cols);
+        app_ref cond(condition, m);
+        return r?alloc(filter_proj_fn, r, t, cond, removed_col_cnt, removed_cols):0;
+    }
+
+
+
+
+}
diff --git a/src/muz/rel/check_relation.h b/src/muz/rel/check_relation.h
new file mode 100644
index 000000000..2856bf3a0
--- /dev/null
+++ b/src/muz/rel/check_relation.h
@@ -0,0 +1,147 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    check_relation.h
+
+Abstract:
+
+    Checked relation. 
+    Each operation on an underlying relation is checked for correctness.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2014-09-23
+
+Revision History:
+
+
+--*/
+
+#ifndef _CHECK_RELATION_H_
+#define _CHECK_RELATION_H_
+
+#include "doc.h"
+#include "dl_base.h"
+
+namespace datalog {
+    class check_relation_plugin;
+    class check_relation;
+    
+    class check_relation : public relation_base {
+        friend class check_relation_plugin;
+        ast_manager&    m;
+        relation_base*  m_relation;
+        expr_ref        m_fml;
+        void check_equiv(expr* f1, expr* f2) const;
+        expr_ref mk_eq(relation_fact const& f) const;
+    public:
+        check_relation(check_relation_plugin& p, relation_signature const& s, relation_base* r);
+        virtual ~check_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 check_relation * clone() const;
+        virtual check_relation * complement(func_decl*) const;
+        virtual void to_formula(expr_ref& fml) const;
+        check_relation_plugin& get_plugin() const; 
+        virtual bool fast_empty() const;
+        virtual bool empty() const; 
+        virtual void display(std::ostream& out) const;
+        virtual bool is_precise() const { return m_relation->is_precise(); }
+        virtual unsigned get_size_estimate_rows() const { return m_relation->get_size_estimate_rows(); }
+        relation_base&  rb() { return *m_relation; }
+        relation_base const& rb() const { return *m_relation; }
+        expr_ref ground(expr* fml) const;
+        void consistent_formula();
+    };
+
+    class check_relation_plugin : public relation_plugin {
+        friend class check_relation;
+        
+        class join_fn;
+        class project_fn;
+        class union_fn;
+        class rename_fn;
+        class filter_equal_fn;
+        class filter_identical_fn;
+        class filter_interpreted_fn;
+        class filter_by_negation_fn;        
+        class filter_by_union_fn;
+        class filter_proj_fn;
+        class negation_filter_fn;
+        ast_manager& m;
+        relation_plugin* m_base;
+        static check_relation& get(relation_base& r);
+        static check_relation* get(relation_base* r);
+        static check_relation const & get(relation_base const& r);   
+    public:
+        check_relation_plugin(relation_manager& rm);
+        ~check_relation_plugin();
+        void set_plugin(relation_plugin* p) { m_base = p; }
+
+        virtual bool can_handle_signature(const relation_signature & s);
+        static symbol get_name() { return symbol("check_relation"); }
+        virtual relation_base * mk_empty(const relation_signature & s);
+        virtual relation_base * mk_full(func_decl* p, const relation_signature & s);
+        virtual relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2,
+            unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
+        virtual relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, 
+            const unsigned * removed_cols);
+        virtual relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len, 
+            const unsigned * permutation_cycle);
+        virtual relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src, 
+            const relation_base * delta);
+        virtual relation_union_fn * mk_widen_fn(const relation_base & tgt, const relation_base & src, 
+            const relation_base * delta);
+        virtual relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, 
+            const unsigned * identical_cols);
+        virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, 
+            unsigned col);
+        virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);
+        virtual relation_intersection_filter_fn * mk_filter_by_negation_fn(
+            const relation_base& t,
+            const relation_base& neg, unsigned joined_col_cnt, const unsigned *t_cols,
+            const unsigned *negated_cols);
+        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 verify_permutation(
+            relation_base const& src, relation_base const& dst, 
+            unsigned_vector const& cycle);
+
+        void verify_project(
+            relation_base const& src, expr* f1, 
+            relation_base const& dst, expr* f2,
+            unsigned_vector const& removed_cols);
+
+        void verify_project(
+            relation_base const& src, 
+            relation_base const& dst, 
+            unsigned_vector const& removed_cols);
+
+        void verify_filter_project(
+            relation_base const& src, relation_base const& dst, 
+            app* cond, unsigned_vector const& removed_cols);
+
+
+
+        void check_equiv(expr* f1, expr* f2);
+
+        
+    };
+};
+       
+#endif /* _CHECK_RELATION_H_ */
+
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index e53dae88a..fa9bc84ee 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -248,6 +248,7 @@ namespace datalog {
         class plugin_object {
             friend class relation_manager;
             friend class check_table_plugin;
+            friend class check_relation_plugin;
 
             family_id m_kind;
             symbol    m_name;
diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index 4122811ac..bf2f09d56 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -759,9 +759,9 @@ namespace datalog {
             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);
             if (!find_fn(r_src, fn)) {
@@ -885,13 +885,12 @@ 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;
             }
-
+            log_verbose(ctx);            
+            ++ctx.m_stats.m_select_equal_project;
             relation_transformer_fn * fn;
             relation_base & r = *ctx.reg(m_src);
             if (!find_fn(r, fn)) {
diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h
index be81a7afa..530538df5 100644
--- a/src/muz/rel/dl_relation_manager.h
+++ b/src/muz/rel/dl_relation_manager.h
@@ -176,6 +176,7 @@ namespace datalog {
         table_plugin * get_table_plugin(symbol const& s);
         relation_plugin * get_relation_plugin(symbol const& s);
         relation_plugin & get_relation_plugin(family_id kind);
+        void              set_favourite_plugin(relation_plugin* p) { m_favourite_relation_plugin = p; }
         table_relation_plugin & get_table_relation_plugin(table_plugin & tp);
         bool try_get_finite_product_relation_plugin(const relation_plugin & inner, 
             finite_product_relation_plugin * & res);
diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 917eeb655..938f39aed 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -25,6 +25,7 @@ Revision History:
 #include "expr_safe_replace.h"
 #include "smt_params.h"
 #include "ast_util.h"
+#include "ast_pp.h"
 
 doc_manager::doc_manager(unsigned n): m(n), m_alloc("doc") {
     m_full = m.allocateX();
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 371e14353..62932a901 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -34,6 +34,7 @@ Revision History:
 #include"dl_finite_product_relation.h"
 #include"product_set.h"
 #include"udoc_relation.h"
+#include"check_relation.h"
 #include"dl_lazy_table.h"
 #include"dl_sparse_table.h"
 #include"dl_table.h"
@@ -118,6 +119,7 @@ namespace datalog {
         rm.register_plugin(alloc(karr_relation_plugin, rm));
         rm.register_plugin(alloc(product_set_plugin, rm));
         rm.register_plugin(alloc(udoc_plugin, rm));
+        rm.register_plugin(alloc(check_relation_plugin, rm));
     }
 
     rel_context::~rel_context() {
@@ -575,6 +577,24 @@ namespace datalog {
         m_ectx.collect_statistics(st);
     }
 
+    void rel_context::updt_params() {
+        if (m_context.check_relation() != symbol::null) {
+            symbol cr("check_relation");
+            m_context.set_default_relation(cr);
+            relation_plugin* p = get_rmanager().get_relation_plugin(cr);
+            SASSERT(p);
+            check_relation_plugin* p1 = dynamic_cast<check_relation_plugin*>(p);
+            relation_plugin* p2 = get_rmanager().get_relation_plugin(m_context.check_relation());
+            SASSERT(p2);
+            SASSERT(p1 != p2);
+            p1->set_plugin(p2);
+            get_rmanager().set_favourite_plugin(p1);
+            if (m_context.check_relation() == symbol("doc")) {
+                m_context.set_unbound_compressor(false);
+            }
+        }
+    }
+
     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 8cdee2766..e445c926f 100644
--- a/src/muz/rel/rel_context.h
+++ b/src/muz/rel/rel_context.h
@@ -84,6 +84,7 @@ namespace datalog {
 
         virtual void cancel() { set_cancel(true); }
         virtual void cleanup() { set_cancel(false);}
+        virtual void updt_params();
 
         /**
            \brief Restrict the set of used predicates to \c res.
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index b5af52701..2bdec8e01 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -402,7 +402,6 @@ 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;
         }
     };
@@ -572,7 +571,6 @@ namespace datalog {
             TRACE("doc", _r.display(tout << "dst':\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) {
@@ -957,8 +955,6 @@ namespace datalog {
             udoc_relation & t = get(tb);
             udoc& u = t.get_udoc();
             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));
@@ -968,7 +964,6 @@ namespace datalog {
             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) {
@@ -1118,13 +1113,6 @@ namespace datalog {
             u2.merge(dm, m_roots, m_equalities, m_col_list);
             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";
@@ -1145,113 +1133,7 @@ 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 6b7a218b5..64ced8e83 100644
--- a/src/muz/rel/udoc_relation.h
+++ b/src/muz/rel/udoc_relation.h
@@ -133,15 +133,6 @@ 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 ad62893d8..3dcf57613 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -262,7 +262,7 @@ class test_doc_cls {
                 rep2.insert(m_vars[i].get(), m.mk_false());
                 rep2(fml, tmp2);
                 if (tmp1 == tmp2) {
-                    fml1 = tmp1;
+                    fml = tmp1;
                 }
                 else {
                     fml = m.mk_or(tmp1, tmp2);
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index 5c25c8ee7..523d4e4db 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -15,6 +15,7 @@
 #include "dl_register_engine.h"
 #include "rel_context.h"
 #include "bv_decl_plugin.h"
+#include "check_relation.h"
 
 
 class udoc_tester {
@@ -41,6 +42,7 @@ class udoc_tester {
     datalog::context          m_ctx;
     datalog::rel_context      rc;
     udoc_plugin&              p;
+    datalog::check_relation_plugin&           cr;
 
 
     tbit choose_tbit() {
@@ -92,9 +94,12 @@ class udoc_tester {
     }
 
 public:
-    udoc_tester(): m_init(m), bv(m), m_vars(m), m_ctx(m, m_reg, m_smt_params), rc(m_ctx),
-                   p(dynamic_cast<udoc_plugin&>(*rc.get_rmanager().get_relation_plugin(symbol("doc"))))
-    {        
+    udoc_tester(): 
+        m_init(m), bv(m), m_vars(m), m_ctx(m, m_reg, m_smt_params), rc(m_ctx),
+        p(dynamic_cast<udoc_plugin&>(*rc.get_rmanager().get_relation_plugin(symbol("doc")))),
+        cr(dynamic_cast<datalog::check_relation_plugin&>(*rc.get_rmanager().get_relation_plugin(symbol("check_relation"))))
+    {   
+        cr.set_plugin(&p);
     }
 
     udoc_relation* mk_empty(relation_signature const& sig) {
@@ -443,7 +448,7 @@ public:
         join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr());
         t = (*join_fn)(*t1, *t2);
 
-        p.verify_join(*t1, *t2, *t, jc1.size(), jc1.c_ptr(), jc2.c_ptr());
+        cr.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);
@@ -707,7 +712,7 @@ public:
         rel_mut fint = p.mk_filter_interpreted_fn(t, cond);
         (*fint)(t);
         t.display(std::cout << "filter: " << mk_pp(cond, m) << " "); std::cout << "\n";
-        t.get_plugin().verify_filter(fml0, t, cond);
+        cr.verify_filter(fml0, t, cond);
         full->deallocate();
     }