diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 1f50bdfea..d0e174914 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -151,7 +151,7 @@ public:
     void set_index(int idx) { m_symbol_index = idx; }
 };
 
-TreeNode* MkToken(alloc_region& r, char* token, int symbolIndex) { 
+TreeNode* MkToken(alloc_region& r, char const* token, int symbolIndex) { 
     TreeNode* ss;
     char* symbol = tptp_lval[symbolIndex];
     ss = new (r) TreeNode(r, symbol, NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL,NULL);
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 11cb48490..3a62a9b98 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -27,6 +27,7 @@ Revision History:
 #include"ast_smt2_pp.h"
 #include"datatype_decl_plugin.h"
 #include"scoped_proof.h"
+#include"fixedpoint_params.hpp"
 
 
 namespace datalog {
@@ -199,7 +200,7 @@ namespace datalog {
         m_register_engine(re),
         m_fparams(fp),
         m_params_ref(pa),
-        m_params(m_params_ref),
+        m_params(alloc(fixedpoint_params, m_params_ref)),
         m_decl_util(m),
         m_rewriter(m),
         m_var_subst(m),
@@ -263,6 +264,31 @@ namespace datalog {
         return *m_sorts.find(s);
     }
 
+
+    bool context::generate_proof_trace() const { return m_params->generate_proof_trace(); }
+    bool context::output_profile() const { return m_params->output_profile(); }
+    bool context::output_tuples() const { return m_params->output_tuples(); }
+    bool context::use_map_names() const { return m_params->use_map_names(); }
+    bool context::fix_unbound_vars() const { return m_params->fix_unbound_vars(); }
+    symbol context::default_table() const { return m_params->default_table(); }
+    symbol context::default_relation() const { return m_params->default_relation(); } // external_relation_plugin::get_name()); 
+    symbol context::default_table_checker() const { return m_params->default_table_checker(); }
+    bool context::default_table_checked() const { return m_params->default_table_checked(); }
+    bool context::dbg_fpr_nonempty_relation_signature() const { return m_params->dbg_fpr_nonempty_relation_signature(); }
+    unsigned context::dl_profile_milliseconds_threshold() const { return m_params->profile_timeout_milliseconds(); }
+    bool context::all_or_nothing_deltas() const { return m_params->all_or_nothing_deltas(); }
+    bool context::compile_with_widening() const { return m_params->compile_with_widening(); }
+    bool context::unbound_compressor() const { return m_params->unbound_compressor(); }
+    bool context::similarity_compressor() const { return m_params->similarity_compressor(); }
+    unsigned context::similarity_compressor_threshold() const { return m_params->similarity_compressor_threshold(); }
+    unsigned context::soft_timeout() const { return m_fparams.m_soft_timeout; }
+    unsigned context::initial_restart_timeout() const { return m_params->initial_restart_timeout(); } 
+    bool context::generate_explanations() const { return m_params->generate_explanations(); }
+    bool context::explanations_on_relation_level() const { return m_params->explanations_on_relation_level(); }
+    bool context::magic_sets_for_queries() const { return m_params->magic_sets_for_queries();  }
+    bool context::eager_emptiness_checking() const { return m_params->eager_emptiness_checking(); }
+
+
     void context::register_finite_sort(sort * s, sort_kind k) {
         m_pinned.push_back(s);
         SASSERT(!m_sorts.contains(s));
@@ -861,7 +887,7 @@ namespace datalog {
     };
 
     void context::configure_engine() {
-        symbol e = m_params.engine();
+        symbol e = m_params->engine();
         
         if (e == symbol("datalog")) {
             m_engine_type = DATALOG_ENGINE;
@@ -1082,9 +1108,9 @@ namespace datalog {
         expr_ref fml(m);
         expr_ref_vector rules(m);
         svector<symbol> names;
-        bool use_fixedpoint_extensions = m_params.print_with_fixedpoint_extensions();
-        bool print_low_level = m_params.print_low_level_smt2();
-        bool do_declare_vars = m_params.print_with_variable_declarations();
+        bool use_fixedpoint_extensions = m_params->print_with_fixedpoint_extensions();
+        bool print_low_level = m_params->print_low_level_smt2();
+        bool do_declare_vars = m_params->print_with_variable_declarations();
 
 #define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);
 
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 97a371f5a..2eb9e0652 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -43,6 +43,8 @@ Revision History:
 #include"expr_functors.h"
 #include"dl_engine_base.h"
 
+struct fixedpoint_params;
+
 namespace datalog {
 
     enum execution_result {
@@ -168,7 +170,7 @@ namespace datalog {
         register_engine_base& m_register_engine;
         smt_params &       m_fparams;
         params_ref         m_params_ref;
-        fixedpoint_params  m_params;
+        fixedpoint_params*  m_params;
         dl_decl_util       m_decl_util;
         th_rewriter        m_rewriter;
         var_subst          m_var_subst;
@@ -231,33 +233,35 @@ namespace datalog {
         ast_manager & get_manager() const { return m; }
         rule_manager & get_rule_manager() { return m_rule_manager; }
         smt_params & get_fparams() const { return m_fparams; }
-        fixedpoint_params const&  get_params() const { return m_params; }
+        fixedpoint_params const&  get_params() const { return *m_params; }
         DL_ENGINE get_engine() { configure_engine(); return m_engine_type; }
         register_engine_base& get_register_engine() { return m_register_engine; }
         th_rewriter& get_rewriter() { return m_rewriter; }
         var_subst & get_var_subst() { return m_var_subst; }
         dl_decl_util & get_decl_util()  { return m_decl_util; }
 
-        bool generate_proof_trace() const { return m_params.generate_proof_trace(); }
-        bool output_profile() const { return m_params.output_profile(); }
-        bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); }
-        symbol default_table() const { return m_params.default_table(); }
-        symbol default_relation() const { return m_params.default_relation(); } // external_relation_plugin::get_name()); 
-        symbol default_table_checker() const { return m_params.default_table_checker(); }
-        bool default_table_checked() const { return m_params.default_table_checked(); }
-        bool dbg_fpr_nonempty_relation_signature() const { return m_params.dbg_fpr_nonempty_relation_signature(); }
-        unsigned dl_profile_milliseconds_threshold() const { return m_params.profile_timeout_milliseconds(); }
-        bool all_or_nothing_deltas() const { return m_params.all_or_nothing_deltas(); }
-        bool compile_with_widening() const { return m_params.compile_with_widening(); }
-        bool unbound_compressor() const { return m_params.unbound_compressor(); }
-        bool similarity_compressor() const { return m_params.similarity_compressor(); }
-        unsigned similarity_compressor_threshold() const { return m_params.similarity_compressor_threshold(); }
-        unsigned soft_timeout() const { return m_fparams.m_soft_timeout; }
-        unsigned initial_restart_timeout() const { return m_params.initial_restart_timeout(); } 
-        bool generate_explanations() const { return m_params.generate_explanations(); }
-        bool explanations_on_relation_level() const { return m_params.explanations_on_relation_level(); }
-        bool magic_sets_for_queries() const { return m_params.magic_sets_for_queries();  }
-        bool eager_emptiness_checking() const { return m_params.eager_emptiness_checking(); }
+        bool generate_proof_trace() const;
+        bool output_profile() const;
+        bool output_tuples() const;
+        bool use_map_names() const;
+        bool fix_unbound_vars() const;
+        symbol default_table() const;
+        symbol default_relation() const;
+        symbol default_table_checker() const;
+        bool default_table_checked() const;
+        bool dbg_fpr_nonempty_relation_signature() const;
+        unsigned dl_profile_milliseconds_threshold() const;
+        bool all_or_nothing_deltas() const;
+        bool compile_with_widening() const;
+        bool unbound_compressor() const;
+        bool similarity_compressor() const;
+        unsigned similarity_compressor_threshold() const;
+        unsigned soft_timeout() const;
+        unsigned initial_restart_timeout() const;
+        bool generate_explanations() const;
+        bool explanations_on_relation_level() const;
+        bool magic_sets_for_queries() const;
+        bool eager_emptiness_checking() const;
 
         void register_finite_sort(sort * s, sort_kind k);
 
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index 2f9eb519c..c23f222e5 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -30,9 +30,32 @@ Revision History:
 #include"dl_context.h"
 #include"dl_rule.h"
 #include"dl_util.h"
+#include"stopwatch.h"
 
 namespace datalog {
 
+    static unsigned verbose_action_inside = 0;
+
+    verbose_action::verbose_action(char const* msg, unsigned lvl): m_lvl(lvl), m_sw(0) {
+        IF_VERBOSE(m_lvl, 
+                   (verbose_stream() << msg << "...").flush(); 
+                   m_sw = alloc(stopwatch); 
+                   m_sw->start(););
+    }
+
+    verbose_action::~verbose_action() {
+        double sec = 0.0;
+        if (m_sw) m_sw->stop();
+        sec = m_sw?m_sw->get_seconds():0.0;
+        if (sec < 0.001) sec = 0.0;
+        IF_VERBOSE(m_lvl, 
+                   (verbose_stream() << sec << "s\n").flush();
+                   );
+        dealloc(m_sw);
+    }
+
+
+
 
     bool contains_var(expr * trm, unsigned var_idx) {
         ptr_vector<sort> vars;
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index f2c50487f..e13e7b53a 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -26,7 +26,6 @@ Revision History:
 #include"horn_subsume_model_converter.h"
 #include"replace_proof_converter.h"
 #include"substitution.h"
-#include"fixedpoint_params.hpp"
 #include"ast_counter.h"
 #include"statistics.h"
 #include"lbool.h"
@@ -43,6 +42,14 @@ namespace datalog {
     class relation_fact;
     class relation_signature;
 
+    class verbose_action {
+        unsigned  m_lvl;
+        class stopwatch* m_sw;
+    public:
+        verbose_action(char const* msg, unsigned lvl = 1);
+        ~verbose_action();
+    };
+
     enum PDR_CACHE_MODE {
         NO_CACHE,
         HASH_CACHE,
@@ -706,29 +713,6 @@ namespace datalog {
         dealloc(ptr);
     }
 
-    template<typename T>
-    class scoped_rel {
-        T* m_t;
-    public:
-        scoped_rel(T* t) : m_t(t) {}
-        ~scoped_rel() { if (m_t) { universal_delete(m_t); } }
-        scoped_rel() : m_t(0) {}
-        scoped_rel& operator=(T* t) { if (m_t) { universal_delete(m_t); } m_t = t;  return *this; }
-        T* operator->() { return m_t; }
-        const T* operator->() const { return m_t; }
-        T& operator*() { return *m_t; }
-        const T& operator*() const { return *m_t; }
-        operator bool() const { return m_t!=0; }
-        T* get() const { return m_t; }
-        /**
-           \brief Remove object from \c scoped_rel without deleting it.
-        */
-        T* release() {
-            T* res = m_t;
-            m_t = 0;
-            return res;
-        }
-    };
 
     /**
        \brief If it is possible to convert the beginning of \c s to uint64,
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 60d285a55..eb4bc72c4 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -32,6 +32,7 @@ Revision History:
 #include "dl_transforms.h"
 #include "dl_mk_rule_inliner.h"
 #include "scoped_proof.h"
+#include"fixedpoint_params.hpp"
 
 namespace datalog {
 
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index 545f3e14a..830f6d078 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -1164,7 +1164,7 @@ public:
         : dparser(ctx, ctx.get_manager()),
           m_bool_sort(ctx.get_manager()),
           m_short_sort(ctx.get_manager()),
-          m_use_map_names(ctx.get_params().use_map_names()) {
+          m_use_map_names(ctx.use_map_names()) {
     }
     ~wpa_parser_impl() {
         reset_dealloc_values(m_sort_contents);
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 7f73b0895..35af38630 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -30,6 +30,7 @@ Notes:
 #include"scoped_ctrl_c.h"
 #include"scoped_timer.h"
 #include"trail.h"
+#include"fixedpoint_params.hpp"
 #include<iomanip>
 
 
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index ca6cbc2fb..0c094c277 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -27,6 +27,7 @@ Revision History:
 #include"dl_mk_slice.h"
 #include"filter_model_converter.h"
 #include"dl_transforms.h"
+#include"fixedpoint_params.hpp"
 
 class horn_tactic : public tactic {
     struct imp {
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index f3e253071..aab7b1388 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -77,9 +77,9 @@ namespace pdr {
     pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): 
         pm(pm), m(pm.get_manager()),
         ctx(ctx), m_head(head, m), 
-        m_sig(m), m_solver(pm, head->get_name()),
+        m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()),
         m_invariants(m), m_transition(m), m_initial_state(m), 
-        m_reachable(pm, pm.get_params()) {}
+        m_reachable(pm, (datalog::PDR_CACHE_MODE)ctx.get_params().cache_mode()) {}
 
     pred_transformer::~pred_transformer() {
         rule2inst::iterator it2 = m_rule2inst.begin(), end2 = m_rule2inst.end();
@@ -1239,7 +1239,7 @@ namespace pdr {
           m_params(params),
           m(m),
           m_context(0),
-          m_pm(m_fparams, params, m),
+          m_pm(m_fparams, params.max_num_contexts(), m),
           m_query_pred(m),
           m_query(0),
           m_search(m_params.bfs_model_search()),
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 57238abb3..8a4f3e438 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -28,6 +28,7 @@ Revision History:
 #include "pdr_manager.h"
 #include "pdr_prop_solver.h"
 #include "pdr_reachable_cache.h"
+#include "fixedpoint_params.hpp"
 
 
 namespace datalog {
diff --git a/src/muz/pdr/pdr_manager.cpp b/src/muz/pdr/pdr_manager.cpp
index 9eb10aba9..bda54dbd7 100644
--- a/src/muz/pdr/pdr_manager.cpp
+++ b/src/muz/pdr/pdr_manager.cpp
@@ -166,14 +166,13 @@ namespace pdr {
         return res;
     }
     
-    manager::manager(smt_params& fparams, fixedpoint_params const& params, ast_manager& manager) :
+    manager::manager(smt_params& fparams, unsigned max_num_contexts, ast_manager& manager) :
         m(manager),
         m_fparams(fparams),
-        m_params(params),
         m_brwr(m),
         m_mux(m, get_state_suffixes()),
         m_background(m.mk_true(), m),
-        m_contexts(fparams, params, m),
+        m_contexts(fparams, max_num_contexts, m),
         m_next_unique_num(0)
     {        
     }
diff --git a/src/muz/pdr/pdr_manager.h b/src/muz/pdr/pdr_manager.h
index cb2c9b253..0e8e890e8 100644
--- a/src/muz/pdr/pdr_manager.h
+++ b/src/muz/pdr/pdr_manager.h
@@ -78,7 +78,6 @@ namespace pdr {
     {
         ast_manager&      m;
         smt_params& m_fparams;
-        fixedpoint_params const& m_params;
         
         mutable bool_rewriter m_brwr;
         
@@ -99,12 +98,10 @@ namespace pdr {
         void add_new_state(func_decl * s);
         
     public:
-        manager(smt_params& fparams, fixedpoint_params const& params, 
-                ast_manager & manager);
+        manager(smt_params& fparams, unsigned max_num_contexts, ast_manager & manager);
         
         ast_manager& get_manager() const { return m; }
         smt_params& get_fparams() const { return m_fparams; }
-        fixedpoint_params const& get_params() const { return m_params; }
         bool_rewriter& get_brwr() const { return m_brwr; }
 
         expr_ref mk_and(unsigned sz, expr* const* exprs);
diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp
index d9b22e04e..8fe8c0e0e 100644
--- a/src/muz/pdr/pdr_prop_solver.cpp
+++ b/src/muz/pdr/pdr_prop_solver.cpp
@@ -30,6 +30,7 @@ Revision History:
 #include "pdr_farkas_learner.h"
 #include "ast_smt2_pp.h"
 #include "expr_replacer.h"
+#include "fixedpoint_params.hpp"
 
 //
 // Auxiliary structure to introduce propositional names for assumptions that are not
@@ -225,12 +226,12 @@ namespace pdr {
     };
 
 
-    prop_solver::prop_solver(manager& pm, symbol const& name) :
+    prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const& name) :
         m_fparams(pm.get_fparams()),
         m(pm.get_manager()),
         m_pm(pm),
         m_name(name),
-        m_try_minimize_core(pm.get_params().try_minimize_core()),
+        m_try_minimize_core(p.try_minimize_core()),
         m_ctx(pm.mk_fresh()),
         m_pos_level_atoms(m),
         m_neg_level_atoms(m),
diff --git a/src/muz/pdr/pdr_prop_solver.h b/src/muz/pdr/pdr_prop_solver.h
index 0c60a7124..a63ec2bf4 100644
--- a/src/muz/pdr/pdr_prop_solver.h
+++ b/src/muz/pdr/pdr_prop_solver.h
@@ -31,6 +31,8 @@ Revision History:
 #include "pdr_manager.h"
 #include "pdr_smt_context_manager.h"
 
+struct fixedpoint_params;
+
 namespace pdr {
     class prop_solver {
     
@@ -73,7 +75,7 @@ namespace pdr {
         
         
     public:
-        prop_solver(pdr::manager& pm, symbol const& name);
+        prop_solver(pdr::manager& pm, fixedpoint_params const& p, symbol const& name);
         
         /** return true is s is a symbol introduced by prop_solver */
         bool is_aux_symbol(func_decl * s) const { 
diff --git a/src/muz/pdr/pdr_reachable_cache.cpp b/src/muz/pdr/pdr_reachable_cache.cpp
index 4f4f620de..85100c19f 100644
--- a/src/muz/pdr/pdr_reachable_cache.cpp
+++ b/src/muz/pdr/pdr_reachable_cache.cpp
@@ -21,13 +21,13 @@ Revision History:
 
 namespace pdr {
 
-    reachable_cache::reachable_cache(pdr::manager & pm, fixedpoint_params const& params)
+    reachable_cache::reachable_cache(pdr::manager & pm, datalog::PDR_CACHE_MODE cm)
         : m(pm.get_manager()), 
           m_pm(pm), 
           m_ctx(0),
           m_ref_holder(m), 
           m_disj_connector(m),
-          m_cache_mode((datalog::PDR_CACHE_MODE)params.cache_mode()) {
+          m_cache_mode(cm) {
         if (m_cache_mode == datalog::CONSTRAINT_CACHE) {
             m_ctx = pm.mk_fresh();
             m_ctx->assert_expr(m_pm.get_background());
diff --git a/src/muz/pdr/pdr_reachable_cache.h b/src/muz/pdr/pdr_reachable_cache.h
index 48caa22a5..aef6f7a4f 100644
--- a/src/muz/pdr/pdr_reachable_cache.h
+++ b/src/muz/pdr/pdr_reachable_cache.h
@@ -47,7 +47,7 @@ namespace pdr {
         void add_disjuncted_formula(expr * f);
         
     public:
-        reachable_cache(pdr::manager & pm, fixedpoint_params const& params);
+        reachable_cache(pdr::manager & pm, datalog::PDR_CACHE_MODE cm);
         
         void add_init(app * f)   { add_disjuncted_formula(f); }
         
diff --git a/src/muz/pdr/pdr_smt_context_manager.cpp b/src/muz/pdr/pdr_smt_context_manager.cpp
index 49ae35423..b6aa8411d 100644
--- a/src/muz/pdr/pdr_smt_context_manager.cpp
+++ b/src/muz/pdr/pdr_smt_context_manager.cpp
@@ -113,10 +113,10 @@ namespace pdr {
         return m_context.get_proof();
     }
 
-    smt_context_manager::smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m):
+    smt_context_manager::smt_context_manager(smt_params& fp, unsigned max_num_contexts, ast_manager& m):
         m_fparams(fp), 
         m(m), 
-        m_max_num_contexts(p.max_num_contexts()),
+        m_max_num_contexts(max_num_contexts),
         m_num_contexts(0), 
         m_predicate_list(m) {
     }
diff --git a/src/muz/pdr/pdr_smt_context_manager.h b/src/muz/pdr/pdr_smt_context_manager.h
index 7d6eebfbd..4775dc58f 100644
--- a/src/muz/pdr/pdr_smt_context_manager.h
+++ b/src/muz/pdr/pdr_smt_context_manager.h
@@ -97,7 +97,7 @@ namespace pdr {
         app_ref_vector           m_predicate_list;
         func_decl_set            m_predicate_set;        
     public:
-        smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m);
+        smt_context_manager(smt_params& fp, unsigned max_num_contexts, ast_manager& m);
         ~smt_context_manager();
         smt_context* mk_fresh();                
         void collect_statistics(statistics& st) const;
diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp
index 4db835bed..d021d5fb1 100644
--- a/src/muz/pdr/pdr_util.cpp
+++ b/src/muz/pdr/pdr_util.cpp
@@ -37,7 +37,6 @@ Notes:
 #include "rewriter_def.h"
 #include "util.h"
 #include "pdr_manager.h"
-#include "pdr_prop_solver.h"
 #include "pdr_util.h"
 #include "arith_decl_plugin.h"
 #include "expr_replacer.h"
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index 1556660d8..d03c94154 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -35,6 +35,30 @@ namespace datalog {
     class context;
     class relation_manager;
 
+    template<typename T>
+    class scoped_rel {
+        T* m_t;
+    public:
+        scoped_rel(T* t) : m_t(t) {}
+        ~scoped_rel() { if (m_t) { universal_delete(m_t); } }
+        scoped_rel() : m_t(0) {}
+        scoped_rel& operator=(T* t) { if (m_t && t != m_t) { universal_delete(m_t); } m_t = t;  return *this; }
+        T* operator->() { return m_t; }
+        const T* operator->() const { return m_t; }
+        T& operator*() { return *m_t; }
+        const T& operator*() const { return *m_t; }
+        operator bool() const { return m_t!=0; }
+        T* get() const { return m_t; }
+        /**
+           \brief Remove object from \c scoped_rel without deleting it.
+        */
+        T* release() {
+            T* res = m_t;
+            m_t = 0;
+            return res;
+        }
+    };
+
     ast_manager & get_ast_manager_from_rel_manager(const relation_manager & rm);
     context & get_context_from_rel_manager(const relation_manager & rm);
 
@@ -208,6 +232,11 @@ namespace datalog {
             virtual void operator()(base_object & t, const base_object & intersected_obj) = 0;
         };
 
+        class intersection_join_filter_fn : public base_fn {
+        public:
+            virtual void operator()(base_object & t, const base_object & inter1, const base_object& inter2) = 0;
+        };
+
         class default_join_project_fn;
 
         /**
@@ -303,6 +332,7 @@ namespace datalog {
         protected:
             //see \c relation_manager for documentation of the operations
 
+
             virtual join_fn * mk_join_fn(const base_object & t1, const base_object & t2,
                 unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { return 0; }
 
@@ -348,10 +378,22 @@ namespace datalog {
                 const unsigned * t_cols, const unsigned * src_cols) 
             { return 0; }
 
+
             virtual intersection_filter_fn * mk_filter_by_negation_fn(const base_object & t, 
                 const base_object & negated_obj, unsigned joined_col_cnt, 
                 const unsigned * t_cols, const unsigned * negated_cols) 
             { return 0; }
+
+            virtual intersection_join_filter_fn * mk_filter_by_negated_join_fn(
+                const base_object & t, 
+                const base_object & src1, 
+                const base_object & src2, 
+                unsigned_vector const& t_cols,
+                unsigned_vector const& src_cols,
+                unsigned_vector const& src1_cols,
+                unsigned_vector const& src2_cols) 
+            { return 0; }
+
         };
 
         class base_ancestor {
@@ -685,6 +727,7 @@ namespace datalog {
     typedef relation_infrastructure::union_fn relation_union_fn;
     typedef relation_infrastructure::mutator_fn relation_mutator_fn;
     typedef relation_infrastructure::intersection_filter_fn relation_intersection_filter_fn;
+    typedef relation_infrastructure::intersection_join_filter_fn relation_intersection_join_filter_fn;
 
     typedef relation_infrastructure::convenient_join_fn convenient_relation_join_fn;
     typedef relation_infrastructure::convenient_join_project_fn convenient_relation_join_project_fn;
@@ -807,6 +850,7 @@ namespace datalog {
     typedef table_infrastructure::union_fn table_union_fn;
     typedef table_infrastructure::mutator_fn table_mutator_fn;
     typedef table_infrastructure::intersection_filter_fn table_intersection_filter_fn;
+    typedef table_infrastructure::intersection_join_filter_fn table_intersection_join_filter_fn;
 
     typedef table_infrastructure::convenient_join_fn convenient_table_join_fn;
     typedef table_infrastructure::convenient_join_project_fn convenient_table_join_project_fn;
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index 931846c35..276e7b836 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -882,7 +882,8 @@ namespace datalog {
             for (unsigned j = 0; j < neg_len; ++j) {
                 expr * e = neg_tail->get_arg(j);
                 if (is_var(e)) {
-                    neg_vars.insert(to_var(e)->get_idx(), e);
+                    unsigned idx = to_var(e)->get_idx();
+                    neg_vars.insert(idx, e);
                 }
             }
         }
@@ -893,7 +894,7 @@ namespace datalog {
                 pos_vars.insert(to_var(e)->get_idx());
             }
         }
-        // add negative variables that are not in positive:
+        // add negative variables that are not in positive
         u_map<expr*>::iterator it = neg_vars.begin(), end = neg_vars.end();
         for (; it != end; ++it) {
             unsigned v = it->m_key;
diff --git a/src/muz/rel/dl_lazy_table.cpp b/src/muz/rel/dl_lazy_table.cpp
new file mode 100644
index 000000000..16dbc2d21
--- /dev/null
+++ b/src/muz/rel/dl_lazy_table.cpp
@@ -0,0 +1,468 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_lazy_table.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-09-04
+
+Revision History:
+
+--*/
+
+#include "dl_lazy_table.h"
+#include "dl_relation_manager.h"
+#include <strstream>
+
+namespace datalog {
+
+    // ------------------
+    // lazy_table_plugin:
+
+    symbol lazy_table_plugin::mk_name(table_plugin& p) {
+        std::ostringstream strm;
+        strm << "lazy_" << p.get_name();
+        return symbol(strm.str().c_str());
+    }
+
+    table_base * lazy_table_plugin::mk_empty(const table_signature & s) {
+        return alloc(lazy_table, alloc(lazy_table_base, *this, m_plugin.mk_empty(s)));
+    }
+
+    lazy_table const& lazy_table_plugin::get(table_base const& tb) { return dynamic_cast<lazy_table const&>(tb); }
+    lazy_table& lazy_table_plugin::get(table_base& tb) { return dynamic_cast<lazy_table&>(tb); }
+    lazy_table const* lazy_table_plugin::get(table_base const* tb) { return dynamic_cast<lazy_table const*>(tb); }
+    lazy_table* lazy_table_plugin::get(table_base* tb) { return dynamic_cast<lazy_table*>(tb); }
+
+    // --------------------------
+    // lazy_table_plugin::join_fn
+
+    class lazy_table_plugin::join_fn : public convenient_table_join_fn {
+    public:
+        join_fn(table_signature const& s1, table_signature const& s2, unsigned col_cnt, 
+                unsigned const* cols1, unsigned const* cols2):
+            convenient_table_join_fn(s1, s2, col_cnt, cols1, cols2) {}
+                                  
+        virtual table_base* operator()(const table_base& _t1, const table_base& _t2) {
+            lazy_table const& t1 = get(_t1);
+            lazy_table const& t2 = get(_t2);
+            lazy_table_plugin& p = t1.get_lplugin();
+            lazy_table_ref* tr = alloc(lazy_table_join, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr(), t1, t2, get_result_signature());
+            return alloc(lazy_table, tr);
+        }
+    };
+
+    table_join_fn * lazy_table_plugin::mk_join_fn(
+        const table_base & t1, const table_base & t2,
+        unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
+        if (check_kind(t1) && check_kind(t2)) {
+            return alloc(join_fn, t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2);
+        }
+        else {
+            return 0;
+        }
+    }
+
+    // ------------------------
+    // lazy_table_plugin::union
+
+    class lazy_table_plugin::union_fn : public table_union_fn {
+    public:
+        void operator()(table_base & _tgt, const table_base & _src, 
+                        table_base * _delta) {
+            lazy_table& tgt = get(_tgt);
+            lazy_table const& src = get(_src);
+            lazy_table* delta = get(_delta);  
+            table_base const* t_src = src.eval();
+            table_base * t_tgt = tgt.eval();
+            table_base * t_delta = delta?delta->eval():0;
+            verbose_action _t("union");
+            table_union_fn* m = tgt.get_lplugin().get_manager().mk_union_fn(*t_tgt, *t_src, t_delta);
+            SASSERT(m);
+            (*m)(*t_tgt, *t_src, t_delta);
+            dealloc(m);                
+        }
+    };
+
+
+    table_union_fn* lazy_table_plugin::mk_union_fn(
+        const table_base & tgt, const table_base & src, 
+        const table_base * delta) {
+        if (check_kind(tgt) && check_kind(src) && (!delta || check_kind(*delta))) {
+            return alloc(union_fn);
+        }
+        else {
+            return 0;
+        }
+    }        
+
+    // --------------------------
+    // lazy_table_plugin::project
+
+    class lazy_table_plugin::project_fn : public convenient_table_project_fn {
+    public:
+        project_fn(table_signature const& orig_sig, unsigned cnt, unsigned const* cols): 
+            convenient_table_project_fn(orig_sig, cnt, cols)
+        {}
+
+        virtual table_base* operator()(table_base const& _t) {
+            lazy_table const& t = get(_t);
+            return alloc(lazy_table, alloc(lazy_table_project, m_removed_cols.size(), m_removed_cols.c_ptr(), t, get_result_signature()));
+        }
+    };
+
+    table_transformer_fn * lazy_table_plugin::mk_project_fn(
+        const table_base & t, unsigned col_cnt, 
+        const unsigned * removed_cols) {
+        if (check_kind(t)) {
+            return alloc(project_fn, t.get_signature(), col_cnt, removed_cols);
+        }
+        else {
+            return 0;
+        }
+    }
+
+    // -------------------------
+    // lazy_table_plugin::rename
+
+    class lazy_table_plugin::rename_fn : public convenient_table_rename_fn {
+    public:
+        rename_fn(table_signature const& orig_sig, unsigned cnt, unsigned const* cols): 
+            convenient_table_rename_fn(orig_sig, cnt, cols)
+        {}
+
+        virtual table_base* operator()(table_base const& _t) {
+            lazy_table const& t = get(_t);
+            return alloc(lazy_table, alloc(lazy_table_rename, m_cycle.size(), m_cycle.c_ptr(), t, get_result_signature()));
+        }
+    };
+    
+    table_transformer_fn * lazy_table_plugin::mk_rename_fn(
+        const table_base & t, unsigned col_cnt, 
+        const unsigned * removed_cols) {
+        if (check_kind(t)) {
+            return alloc(rename_fn, t.get_signature(), col_cnt, removed_cols);
+        }
+        else {
+            return 0;
+        }
+    }
+
+
+    // -----------------------------------
+    // lazy_table_plugin::filter_identical
+
+    class lazy_table_plugin::filter_identical_fn : public table_mutator_fn {
+        unsigned_vector          m_cols;
+    public:
+        filter_identical_fn(unsigned cnt, unsigned const* cols): m_cols(cnt, cols) {}
+        
+        virtual void operator()(table_base& _t) {
+            lazy_table& t = get(_t);
+            t.set(alloc(lazy_table_filter_identical, m_cols.size(), m_cols.c_ptr(), t));
+        }
+    };
+    
+    table_mutator_fn * lazy_table_plugin::mk_filter_identical_fn(
+        const table_base & t, unsigned col_cnt, const unsigned * identical_cols) {
+        if (check_kind(t)) {
+            return alloc(filter_identical_fn, col_cnt, identical_cols);
+        }
+        else {
+            return 0;
+        }
+    }
+
+
+    // -------------------------------------
+    // lazy_table_plugin::filter_interpreted
+
+    class lazy_table_plugin::filter_interpreted_fn : public table_mutator_fn {
+        app_ref  m_condition;
+    public:
+        filter_interpreted_fn(app_ref& p): m_condition(p) {}
+
+        virtual void operator()(table_base& _t) {
+            lazy_table& t = get(_t);
+            t.set(alloc(lazy_table_filter_interpreted, t, m_condition));
+        }
+    };
+    
+    table_mutator_fn * lazy_table_plugin::mk_filter_interpreted_fn(
+        const table_base & t, app* condition) {
+        if (check_kind(t)) {
+            app_ref cond(condition, get_ast_manager());
+            return alloc(filter_interpreted_fn, cond);
+        }
+        else {
+            return 0;
+        }
+    }
+    
+    // -------------------------------------
+    // lazy_table_plugin::filter_by_negation
+
+    class lazy_table_plugin::filter_by_negation_fn : public table_intersection_filter_fn {
+        unsigned_vector m_cols1;
+        unsigned_vector m_cols2;
+    public:
+        filter_by_negation_fn(unsigned cnt, unsigned const* cols1, unsigned const* cols2):
+            m_cols1(cnt, cols1), m_cols2(cnt, cols2) {}
+        virtual void operator()(table_base & _t, const table_base & _intersected_obj) {
+            lazy_table& t = get(_t);
+            lazy_table const& it = get(_intersected_obj);
+            t.set(alloc(lazy_table_filter_by_negation, t, it, m_cols1, m_cols2));
+        }
+    };
+
+    table_intersection_filter_fn * lazy_table_plugin::mk_filter_by_negation_fn(
+        const table_base & t, 
+        const table_base & negated_obj, unsigned joined_col_cnt, 
+        const unsigned * t_cols, const unsigned * negated_cols) {
+        if (check_kind(t) && check_kind(negated_obj)) {
+            return alloc(filter_by_negation_fn, joined_col_cnt, t_cols, negated_cols);
+        }
+        else {
+            return 0;
+        }
+    }
+
+
+    // -------------------------------
+    // lazy_table_plugin::filter_equal
+
+    class lazy_table_plugin::filter_equal_fn : public table_mutator_fn {
+        table_element m_value;
+        unsigned m_col;
+    public:
+        filter_equal_fn(const table_element & value, unsigned col): 
+            m_value(value),
+            m_col(col)
+        { }
+
+        virtual void operator()(table_base& _t) {
+            lazy_table& t = get(_t);
+            t.set(alloc(lazy_table_filter_equal, m_col, m_value, t));
+        }
+    };
+    
+    table_mutator_fn * lazy_table_plugin::mk_filter_equal_fn(
+        const table_base & t, const table_element & value, unsigned col) {
+        if (check_kind(t)) {
+            return alloc(filter_equal_fn, value, col);
+        }
+        else {
+            return 0;
+        }
+    }
+
+    table_plugin* lazy_table_plugin::mk_sparse(relation_manager& rm) {
+        table_plugin* sp = rm.get_table_plugin(symbol("sparse"));
+        SASSERT(sp);
+        if (sp) {
+            return alloc(lazy_table_plugin, *sp);
+        }
+        else {
+            return 0;
+        }
+    }
+
+
+    // ----------
+    // lazy_table
+    
+    table_base * lazy_table::clone() const {
+        table_base* t = eval();
+        verbose_action _t("clone");
+        return alloc(lazy_table, alloc(lazy_table_base, get_lplugin(), t->clone()));
+    }
+    table_base * lazy_table::complement(func_decl* p, const table_element * func_columns) const {
+        table_base* t = eval()->complement(p, func_columns);
+        return alloc(lazy_table, alloc(lazy_table_base, get_lplugin(), t));
+    }
+    bool lazy_table::empty() const {
+        return m_ref->eval()->empty();
+    }
+    bool lazy_table::contains_fact(const table_fact & f) const {
+        return m_ref->eval()->contains_fact(f);
+    }
+    void lazy_table::remove_fact(table_element const* fact) {
+        m_ref->eval()->remove_fact(fact);
+    }
+    void lazy_table::remove_facts(unsigned fact_cnt, const table_fact * facts) {
+        m_ref->eval()->remove_facts(fact_cnt, facts);
+    }
+    void lazy_table::remove_facts(unsigned fact_cnt, const table_element * facts) {
+        m_ref->eval()->remove_facts(fact_cnt, facts);
+    }
+    void lazy_table::reset() {
+        m_ref = alloc(lazy_table_base, get_lplugin(), get_lplugin().m_plugin.mk_empty(get_signature()));
+    }
+    void lazy_table::add_fact(table_fact const& f) {
+        m_ref->eval()->add_fact(f);
+    }
+    table_base::iterator lazy_table::begin() const {
+        return eval()->begin();
+    }
+    table_base::iterator lazy_table::end() const {
+        return eval()->end();
+    }
+    table_base* lazy_table::eval() const {
+        return m_ref->eval();
+    }
+
+    // -------------------------
+    // eval
+
+
+    table_base* lazy_table_join::force() {
+        SASSERT(!m_table);
+        table_base* t1 = m_t1->eval();
+        table_base* t2 = m_t2->eval();
+        verbose_action _t("join");
+        table_join_fn* join = rm().mk_join_fn(*t1, *t2, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr());
+        m_table = (*join)(*t1, *t2);
+        dealloc(join);        
+        return m_table.get();
+    }
+
+    table_base* lazy_table_project::force() {
+        SASSERT(!m_table);
+        switch(m_src->kind()) {
+        case LAZY_TABLE_JOIN: {
+            lazy_table_join& src = dynamic_cast<lazy_table_join&>(*m_src);
+            table_base* t1 = src.t1()->eval();
+            table_base* t2 = src.t2()->eval();
+            table_join_fn* j_fn = rm().mk_join_project_fn(*t1, *t2, src.cols1(), src.cols2(), m_cols);
+            if (j_fn) {
+                verbose_action _t("join_project");
+                m_table = (*j_fn)(*t1, *t2);
+                dealloc(j_fn);
+            }
+            break;
+        }
+        case LAZY_TABLE_FILTER_INTERPRETED: {
+            lazy_table_filter_interpreted& src = dynamic_cast<lazy_table_filter_interpreted&>(*m_src);
+            table_transformer_fn* tr = rm().mk_filter_interpreted_and_project_fn(*src.eval(), src.condition(), m_cols.size(), m_cols.c_ptr());
+            if (tr) {
+                verbose_action _t("filter_interpreted_project");
+                m_table = (*tr)(*src.eval());
+                dealloc(tr);
+            }
+            break;
+        }
+        case LAZY_TABLE_FILTER_EQUAL: {
+            lazy_table_filter_equal& src = dynamic_cast<lazy_table_filter_equal&>(*m_src);
+            table_base* t = src.eval();
+            table_transformer_fn* tr = rm().mk_select_equal_and_project_fn(*t, src.value(), src.col());
+            if (tr) {
+                verbose_action _t("select_equal_project");
+                m_table = (*tr)(*t);
+                dealloc(tr);
+            }
+            break;
+        }
+        default:
+            break;
+        }
+        if (m_table) {
+            return m_table.get();
+        }
+        table_base* src = m_src->eval();
+        verbose_action _t("project");
+        table_transformer_fn* project = rm().mk_project_fn(*src, m_cols.size(), m_cols.c_ptr());
+        SASSERT(project);
+        m_table = (*project)(*src);
+        dealloc(project);            
+        return m_table.get();
+    }
+
+    table_base* lazy_table_rename::force() {
+        SASSERT(!m_table);
+        table_base* src = m_src->eval();
+        verbose_action _t("rename");
+        table_transformer_fn* rename = rm().mk_rename_fn(*src, m_cols.size(), m_cols.c_ptr());
+        m_table = (*rename)(*src);
+        dealloc(rename);                    
+        return m_table.get();
+    }
+    
+    table_base* lazy_table_filter_identical::force() {
+        SASSERT(!m_table);
+        m_table = m_src->eval();
+        m_src->release_table();
+        m_src = 0;
+        verbose_action _t("filter_identical");
+        table_mutator_fn* m = rm().mk_filter_identical_fn(*m_table, m_cols.size(), m_cols.c_ptr());
+        SASSERT(m);
+        (*m)(*m_table);
+        dealloc(m);                    
+        return m_table.get();
+    }
+
+    table_base* lazy_table_filter_equal::force() {
+        SASSERT(!m_table);
+        m_table = m_src->eval();
+        m_src->release_table();
+        m_src = 0;
+        verbose_action _t("filter_equal");
+        table_mutator_fn* m = rm().mk_filter_equal_fn(*m_table, m_value, m_col);
+        SASSERT(m);
+        (*m)(*m_table);
+        dealloc(m);                
+        return m_table.get();
+    }
+
+    table_base* lazy_table_filter_interpreted::force() {
+        SASSERT(!m_table);
+        m_table = m_src->eval();
+        m_src->release_table();
+        m_src = 0;
+        verbose_action _t("filter_interpreted");
+        table_mutator_fn* m = rm().mk_filter_interpreted_fn(*m_table, m_condition);
+        SASSERT(m);
+        (*m)(*m_table);
+        dealloc(m);                
+        return m_table.get();
+    }
+
+    table_base* lazy_table_filter_by_negation::force() {
+        SASSERT(!m_table);
+        m_table = m_tgt->eval();
+        m_tgt->release_table();
+        m_tgt = 0;
+
+        switch(m_src->kind()) {
+
+        case LAZY_TABLE_JOIN: {
+            lazy_table_join& src = dynamic_cast<lazy_table_join&>(*m_src);
+            table_base* t1 = src.t1()->eval();
+            table_base* t2 = src.t2()->eval();
+            verbose_action _t("filter_by_negation_join");
+            table_intersection_join_filter_fn* jn = rm().mk_filter_by_negated_join_fn(*m_table, *t1, *t2, cols1(), cols2(), src.cols1(), src.cols2());
+            if (jn) {
+                (*jn)(*m_table, *t1, *t2);
+                dealloc(jn);                
+                return m_table.get();
+            }
+            break;
+        }
+        default:
+            break;
+        }
+        table_base* src = m_src->eval();
+        verbose_action _t("filter_by_negation");
+        table_intersection_filter_fn* m = rm().mk_filter_by_negation_fn(*m_table, *src, m_cols1, m_cols2);
+        SASSERT(m);
+        (*m)(*m_table, *src);
+        dealloc(m);                    
+        return m_table.get();
+    }
+}
diff --git a/src/muz/rel/dl_lazy_table.h b/src/muz/rel/dl_lazy_table.h
new file mode 100644
index 000000000..34a8b6b92
--- /dev/null
+++ b/src/muz/rel/dl_lazy_table.h
@@ -0,0 +1,305 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_lazy_table.h
+
+Abstract:
+
+    Structure for delaying table operations.
+    
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-09-04
+
+Revision History:
+
+--*/
+
+#ifndef _DL_LAZY_TABLE_H_
+#define _DL_LAZY_TABLE_H_
+
+#include "dl_base.h"
+#include "ref.h"
+
+namespace datalog {
+    
+    class lazy_table;
+    
+    class lazy_table_plugin : public table_plugin {
+        friend class lazy_table;
+        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;
+        
+        table_plugin& m_plugin;
+        
+        static symbol mk_name(table_plugin& p);
+        
+    public:
+        lazy_table_plugin(table_plugin& p): 
+            table_plugin(mk_name(p), p.get_manager()), 
+            m_plugin(p) {}
+        
+        virtual bool can_handle_signature(const table_signature & s) {
+            return m_plugin.can_handle_signature(s);
+        } 
+        
+        virtual table_base * mk_empty(const table_signature & s);
+                
+        virtual void set_cancel(bool f) { m_plugin.set_cancel(f); }
+
+        static table_plugin* mk_sparse(relation_manager& rm);
+        
+    protected:
+        virtual table_join_fn * mk_join_fn(
+            const table_base & t1, const table_base & t2,
+            unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
+        virtual table_union_fn * mk_union_fn(
+            const table_base & tgt, const table_base & src, 
+            const table_base * delta);
+        virtual table_transformer_fn * mk_project_fn(
+            const table_base & t, unsigned col_cnt, 
+            const unsigned * removed_cols);
+        virtual table_transformer_fn * mk_rename_fn(
+            const table_base & t, unsigned permutation_cycle_len,
+            const unsigned * permutation_cycle);
+        virtual table_mutator_fn * mk_filter_identical_fn(
+            const table_base & t, unsigned col_cnt, const unsigned * identical_cols);
+        virtual table_mutator_fn * mk_filter_equal_fn(
+            const table_base & t, const table_element & value, unsigned col);
+        virtual table_mutator_fn * mk_filter_interpreted_fn(
+            const table_base & t, app * condition);
+        virtual table_intersection_filter_fn * mk_filter_by_negation_fn(
+            const table_base & t, 
+            const table_base & negated_obj, unsigned joined_col_cnt, 
+            const unsigned * t_cols, const unsigned * negated_cols);        
+
+        static lazy_table const& get(table_base const& tb);
+        static lazy_table& get(table_base& tb);
+        static lazy_table const* get(table_base const* tb);
+        static lazy_table* get(table_base* tb);           
+    };
+
+    enum lazy_table_kind {
+        LAZY_TABLE_BASE,
+        LAZY_TABLE_JOIN,
+        LAZY_TABLE_PROJECT,
+        LAZY_TABLE_RENAME,
+        LAZY_TABLE_FILTER_IDENTICAL,
+        LAZY_TABLE_FILTER_EQUAL,
+        LAZY_TABLE_FILTER_INTERPRETED,
+        LAZY_TABLE_FILTER_BY_NEGATION
+    };
+
+    class lazy_table_ref {
+    protected:
+        lazy_table_plugin&     m_plugin;
+        table_signature        m_signature;
+        unsigned               m_ref;
+        scoped_rel<table_base> m_table;
+        relation_manager&  rm() { return m_plugin.get_manager(); }
+        virtual table_base* force() = 0;
+    public:
+        lazy_table_ref(lazy_table_plugin& p, table_signature const& sig): 
+            m_plugin(p), m_signature(sig), m_ref(0) {}
+        virtual ~lazy_table_ref() {}
+        void inc_ref() { ++m_ref; }
+        void dec_ref() { --m_ref; if (0 == m_ref) dealloc(this);  }
+        void release_table() { m_table.release(); }
+
+        virtual lazy_table_kind kind() const = 0;
+        table_signature const& get_signature() const { return m_signature; }
+        lazy_table_plugin & get_lplugin() const { return m_plugin; }
+        table_base* eval() { if (!m_table) { m_table = force(); } SASSERT(m_table); return m_table.get(); }
+    };
+
+    class lazy_table : public table_base {
+    protected:
+        mutable ref<lazy_table_ref> m_ref;
+
+    public:
+        lazy_table(lazy_table_ref* t):
+            table_base(t->get_lplugin(), t->get_signature()), 
+            m_ref(t)
+        {}
+
+        virtual ~lazy_table() {}
+
+        lazy_table_plugin& get_lplugin() const { 
+            return dynamic_cast<lazy_table_plugin&>(table_base::get_plugin()); 
+        }
+
+        virtual table_base * clone() const;
+        virtual table_base * complement(func_decl* p, const table_element * func_columns = 0) const;
+        virtual bool empty() const;
+        virtual bool contains_fact(const table_fact & f) const;
+        virtual void remove_fact(table_element const* fact);
+        virtual void remove_facts(unsigned fact_cnt, const table_fact * facts);
+        virtual void remove_facts(unsigned fact_cnt, const table_element * facts);
+        virtual void reset();
+        virtual void add_fact(table_fact const& f);
+       
+        virtual unsigned get_size_estimate_rows() const { return 1; }
+        virtual unsigned get_size_estimate_bytes() const { return 1; }
+        virtual bool knows_exact_size() const { return false; }
+
+        table_base* eval() const;
+
+        virtual table_base::iterator begin() const;
+        virtual table_base::iterator end() const;
+
+        lazy_table_ref* ref() const { return m_ref.get(); }
+        void set(lazy_table_ref* r) { m_ref = r; }
+    };
+
+    class lazy_table_base : public lazy_table_ref {
+    public:
+        lazy_table_base(lazy_table_plugin & p, table_base* table)
+            : lazy_table_ref(p, table->get_signature()) {
+            m_table = table;
+            // SASSERT(&p.m_plugin == &table->get_lplugin());
+        }
+        virtual ~lazy_table_base() {}
+        virtual lazy_table_kind kind() const { return LAZY_TABLE_BASE; }
+        virtual table_base* force() { return m_table.get(); }       
+    };
+
+    class lazy_table_join : public lazy_table_ref {
+        unsigned_vector m_cols1;
+        unsigned_vector m_cols2;
+        ref<lazy_table_ref>     m_t1;
+        ref<lazy_table_ref>     m_t2;
+    public:
+        lazy_table_join(unsigned col_cnt, 
+                        const unsigned * cols1, const unsigned * cols2, 
+                        lazy_table const& t1, lazy_table const& t2, table_signature const& sig) 
+            : lazy_table_ref(t1.get_lplugin(), sig), 
+              m_cols1(col_cnt, cols1), 
+              m_cols2(col_cnt, cols2),
+              m_t1(t1.ref()),
+              m_t2(t2.ref()) { }
+        virtual ~lazy_table_join() {}
+        virtual lazy_table_kind kind() const { return LAZY_TABLE_JOIN; }
+        unsigned_vector const& cols1() const { return m_cols1; }
+        unsigned_vector const& cols2() const { return m_cols2; }
+        lazy_table_ref* t1() const { return m_t1.get(); }
+        lazy_table_ref* t2() const { return m_t2.get(); }
+        virtual table_base* force();
+    };
+
+
+    class lazy_table_project : public lazy_table_ref {
+        unsigned_vector         m_cols;
+        ref<lazy_table_ref>     m_src;
+    public:
+        lazy_table_project(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig)
+            : lazy_table_ref(src.get_lplugin(), sig), 
+              m_cols(col_cnt, cols), 
+              m_src(src.ref()) {}
+        virtual ~lazy_table_project() {}
+        
+        virtual lazy_table_kind kind() const { return LAZY_TABLE_PROJECT; }
+        unsigned_vector const& cols() const { return m_cols; }
+        lazy_table_ref* src() const { return m_src.get(); }
+        virtual table_base* force();
+    };
+
+    class lazy_table_rename : public lazy_table_ref {
+        unsigned_vector         m_cols;
+        ref<lazy_table_ref>     m_src;
+    public:
+        lazy_table_rename(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig)
+            : lazy_table_ref(src.get_lplugin(), sig), 
+              m_cols(col_cnt, cols), 
+              m_src(src.ref()) {}
+        virtual ~lazy_table_rename() {}
+        
+        virtual lazy_table_kind kind() const { return LAZY_TABLE_RENAME; }
+        unsigned_vector const& cols() const { return m_cols; }
+        lazy_table_ref* src() const { return m_src.get(); }
+        virtual table_base* force();
+    };
+
+    class lazy_table_filter_identical : public lazy_table_ref {
+        unsigned_vector          m_cols;
+        ref<lazy_table_ref>      m_src;
+    public:
+        lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src)
+            : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.ref()) {}
+        virtual ~lazy_table_filter_identical() {}
+        
+        virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_IDENTICAL; }
+        unsigned_vector const& cols() const { return m_cols; }
+        lazy_table_ref* src() const { return m_src.get(); }
+        virtual table_base* force();
+    };
+
+    class lazy_table_filter_equal : public lazy_table_ref {
+        unsigned                  m_col;
+        table_element             m_value;
+        ref<lazy_table_ref>       m_src;
+    public:
+        lazy_table_filter_equal(unsigned col, table_element value, lazy_table const& src)
+            : lazy_table_ref(src.get_lplugin(), src.get_signature()), 
+            m_col(col), 
+            m_value(value), 
+            m_src(src.ref()) {}
+        virtual ~lazy_table_filter_equal() {}
+        
+        virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_EQUAL; }
+        unsigned        col() const { return m_col; }
+        table_element   value() const { return m_value; }
+        lazy_table_ref* src() const { return m_src.get(); }
+        virtual table_base* force();
+    };
+
+    class lazy_table_filter_interpreted : public lazy_table_ref {
+        app_ref                  m_condition;
+        ref<lazy_table_ref>      m_src;
+    public:
+        lazy_table_filter_interpreted(lazy_table const& src, app* condition)
+            : lazy_table_ref(src.get_lplugin(), src.get_signature()), 
+              m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.ref()) {}
+        virtual ~lazy_table_filter_interpreted() {}
+        
+        virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_INTERPRETED; }
+        app* condition() const { return m_condition; }        
+        lazy_table_ref* src() const { return m_src.get(); }
+        virtual table_base* force();
+    };
+
+
+    class lazy_table_filter_by_negation : public lazy_table_ref {
+        ref<lazy_table_ref>       m_tgt;
+        ref<lazy_table_ref>       m_src;
+        unsigned_vector           m_cols1;
+        unsigned_vector           m_cols2;
+    public:
+        lazy_table_filter_by_negation(lazy_table const& tgt, lazy_table const& src, 
+                                      unsigned_vector const& c1, unsigned_vector const& c2) 
+        : lazy_table_ref(tgt.get_lplugin(), tgt.get_signature()),
+            m_tgt(tgt.ref()), 
+            m_src(src.ref()), 
+            m_cols1(c1),
+            m_cols2(c2) {}
+        virtual ~lazy_table_filter_by_negation() {}
+        virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_BY_NEGATION; }
+        lazy_table_ref* tgt() const { return m_tgt.get(); }
+        lazy_table_ref* src() const { return m_src.get(); }
+        unsigned_vector const& cols1() const { return m_cols1; }
+        unsigned_vector const& cols2() const { return m_cols2; }
+        virtual table_base* force();
+    };
+
+
+}
+
+#endif 
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 457ef28c0..9421b26df 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -167,8 +167,13 @@ namespace datalog {
         register_relation_plugin_impl(tr_plugin);
         m_table_relation_plugins.insert(plugin, tr_plugin);
 
+        if (plugin->get_name()==get_context().default_table()) {
+            m_favourite_table_plugin    = plugin;
+            m_favourite_relation_plugin = tr_plugin;
+        }
+
         symbol checker_name = get_context().default_table_checker();
-        if(get_context().default_table_checked() && get_table_plugin(checker_name)) {
+        if (get_context().default_table_checked() && get_table_plugin(checker_name)) {
             if( m_favourite_table_plugin &&
                 (plugin==m_favourite_table_plugin || plugin->get_name()==checker_name) ) {
                 symbol checked_name = get_context().default_table();
@@ -178,7 +183,7 @@ namespace datalog {
                 register_plugin(checking_plugin);
                 m_favourite_table_plugin = checking_plugin;
             }
-            if(m_favourite_relation_plugin && m_favourite_relation_plugin->from_table()) {
+            if (m_favourite_relation_plugin && m_favourite_relation_plugin->from_table()) {
                 table_relation_plugin * fav_rel_plugin = 
                     static_cast<table_relation_plugin *>(m_favourite_relation_plugin);
                 if(&fav_rel_plugin->get_table_plugin()==plugin || plugin->get_name()==checker_name) {
@@ -577,6 +582,7 @@ namespace datalog {
         relation_plugin * p2 = &t2.get_plugin();
 
         relation_join_fn * res = p1->mk_join_fn(t1, t2, col_cnt, cols1, cols2);
+        
         if(!res && p1!=p2) {
             res = p2->mk_join_fn(t1, t2, col_cnt, cols1, cols2);
         }
@@ -1538,6 +1544,19 @@ namespace datalog {
         return res;
     }
 
+    
+    table_intersection_join_filter_fn* relation_manager::mk_filter_by_negated_join_fn(
+        const table_base & t, 
+        const table_base & src1, 
+        const table_base & src2, 
+        unsigned_vector const& t_cols,
+        unsigned_vector const& src_cols,
+        unsigned_vector const& src1_cols,
+        unsigned_vector const& src2_cols) {
+        return t.get_plugin().mk_filter_by_negated_join_fn(t, src1, src2, t_cols, src_cols, src1_cols, src2_cols);
+    }
+
+
 
     class relation_manager::default_table_select_equal_and_project_fn : public table_transformer_fn {
         scoped_ptr<table_mutator_fn> m_filter;
diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h
index 9f12b4bb6..2c148c5e6 100644
--- a/src/muz/rel/dl_relation_manager.h
+++ b/src/muz/rel/dl_relation_manager.h
@@ -564,6 +564,19 @@ namespace datalog {
             return mk_filter_by_negation_fn(t, negated_obj, t_cols.size(), t_cols.c_ptr(), negated_cols.c_ptr());
         }
 
+        /**
+           combined filter by negation with a join.
+         */
+        table_intersection_join_filter_fn* mk_filter_by_negated_join_fn(
+            const table_base & t, 
+            const table_base & src1, 
+            const table_base & src2, 
+            unsigned_vector const& t_cols,
+            unsigned_vector const& src_cols,
+            unsigned_vector const& src1_cols,
+            unsigned_vector const& src2_cols);
+
+
         /**
             \c t must contain at least one functional column.
 
diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp
index 2cae7771f..3b2dc333a 100644
--- a/src/muz/rel/dl_sparse_table.cpp
+++ b/src/muz/rel/dl_sparse_table.cpp
@@ -24,6 +24,7 @@ Revision History:
 
 namespace datalog {
 
+
     // -----------------------------------
     //
     // entry_storage
@@ -415,7 +416,7 @@ namespace datalog {
             }
             //We will change the content of the reserve; which does not change the 'high-level' 
             //content of the table.
-            sparse_table & t = const_cast<sparse_table &>(m_table);
+            sparse_table & t = const_cast<sparse_table&>(m_table);
             t.write_into_reserve(m_key_fact.c_ptr());
 
             store_offset res;
@@ -461,6 +462,8 @@ namespace datalog {
 
     sparse_table::key_indexer& sparse_table::get_key_indexer(unsigned key_len, 
             const unsigned * key_cols) const {
+            verbose_action  _va("get_key_indexer");
+
 #if Z3DEBUG
         //We allow indexes only on non-functional columns because we want to be able to modify them 
         //without having to worry about updating indexes.
@@ -506,6 +509,7 @@ namespace datalog {
     }
 
     bool sparse_table::add_fact(const char * data) {
+        verbose_action  _va("add_fact", 3);
         m_data.write_into_reserve(data);
         return add_reserve_content();
     }
@@ -520,6 +524,7 @@ namespace datalog {
     }
 
     bool sparse_table::contains_fact(const table_fact & f) const {
+        verbose_action  _va("contains_fact", 2);
         sparse_table & t = const_cast<sparse_table &>(*this);
         t.write_into_reserve(f.c_ptr());
         unsigned func_col_cnt = get_signature().functional_columns();
@@ -542,6 +547,7 @@ namespace datalog {
     }
 
     bool sparse_table::fetch_fact(table_fact & f) const {
+        verbose_action  _va("fetch_fact", 2);
         const table_signature & sig = get_signature();
         SASSERT(f.size() == sig.size());
         if (sig.functional_columns() == 0) {
@@ -567,6 +573,7 @@ namespace datalog {
        This is ok as long as we do not allow indexing on functional columns.
     */
     void sparse_table::ensure_fact(const table_fact & f) {
+        verbose_action  _va("ensure_fact", 2);
         const table_signature & sig = get_signature();
         if (sig.functional_columns() == 0) {
             add_fact(f);
@@ -586,6 +593,7 @@ namespace datalog {
     }
 
     void sparse_table::remove_fact(const table_element*  f) {
+        verbose_action  _va("remove_fact", 2);
         //first insert the fact so that we find it's original location and remove it
         write_into_reserve(f);
         if (!m_data.remove_reserve_content()) {
@@ -638,6 +646,7 @@ namespace datalog {
             unsigned joined_col_cnt, const unsigned * t1_joined_cols, const unsigned * t2_joined_cols,
             const unsigned * removed_cols, bool tables_swapped, sparse_table & result) {
 
+        verbose_action _va("join_project", 1);
         unsigned t1_entry_size = t1.m_fact_size;
         unsigned t2_entry_size = t2.m_fact_size;
 
@@ -737,15 +746,21 @@ namespace datalog {
         reset();
     }
 
+    sparse_table const& sparse_table_plugin::get(table_base const& t) { return dynamic_cast<sparse_table const&>(t); }
+    sparse_table& sparse_table_plugin::get(table_base& t) { return dynamic_cast<sparse_table&>(t); }
+    sparse_table const* sparse_table_plugin::get(table_base const* t) { return dynamic_cast<sparse_table const*>(t); }
+    sparse_table* sparse_table_plugin::get(table_base* t) { return dynamic_cast<sparse_table*>(t); }
+
+
     void sparse_table_plugin::reset() {
         table_pool::iterator it = m_pool.begin();
         table_pool::iterator end = m_pool.end();
         for (; it!=end; ++it) {
             sp_table_vector * vect = it->m_value;
-            sp_table_vector::iterator it = vect->begin();
-            sp_table_vector::iterator end = vect->end();
-            for (; it!=end; ++it) {
-                (*it)->destroy(); //calling deallocate() would only put the table back into the pool
+            sp_table_vector::iterator vit = vect->begin();
+            sp_table_vector::iterator vend = vect->end();
+            for (; vit!=vend; ++vit) {
+                (*vit)->destroy(); //calling deallocate() would only put the table back into the pool
             }
             dealloc(vect);
         }
@@ -759,6 +774,7 @@ namespace datalog {
     }
 
     void sparse_table_plugin::recycle(sparse_table * t) {
+        verbose_action  _va("recycle", 2);
         const table_signature & sig = t->get_signature();
         t->reset();
 
@@ -785,7 +801,7 @@ namespace datalog {
     }
 
     sparse_table * sparse_table_plugin::mk_clone(const sparse_table & t) {
-        sparse_table * res = static_cast<sparse_table *>(mk_empty(t.get_signature()));
+        sparse_table * res = get(mk_empty(t.get_signature()));
         res->m_data = t.m_data;
         return res;
     }
@@ -813,12 +829,13 @@ namespace datalog {
 
         virtual table_base * operator()(const table_base & tb1, const table_base & tb2) {
 
-            const sparse_table & t1 = static_cast<const sparse_table &>(tb1);
-            const sparse_table & t2 = static_cast<const sparse_table &>(tb2);
+            verbose_action  _va("join_project");
+            const sparse_table & t1 = get(tb1);
+            const sparse_table & t2 = get(tb2);
 
             sparse_table_plugin & plugin = t1.get_plugin();
 
-            sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
+            sparse_table * res = get(plugin.mk_empty(get_result_signature()));
 
             //If we join with some intersection, want to iterate over the smaller table and
             //do indexing into the bigger one. If we simply do a product, we want the bigger
@@ -868,10 +885,10 @@ namespace datalog {
     class sparse_table_plugin::union_fn : public table_union_fn {
     public:
         virtual void operator()(table_base & tgt0, const table_base & src0, table_base * delta0) {
-
-            sparse_table & tgt = static_cast<sparse_table &>(tgt0);
-            const sparse_table & src = static_cast<const sparse_table &>(src0);
-            sparse_table * delta = static_cast<sparse_table *>(delta0);
+            verbose_action  _va("union");
+            sparse_table & tgt = get(tgt0);
+            const sparse_table & src = get(src0);
+            sparse_table * delta = get(delta0);
 
             unsigned fact_size = tgt.m_fact_size;
             const char* ptr = src.m_data.begin();
@@ -927,12 +944,13 @@ namespace datalog {
         }
 
         virtual table_base * operator()(const table_base & tb) {
-            const sparse_table & t = static_cast<const sparse_table &>(tb);
+            verbose_action  _va("project");
+            const sparse_table & t = get(tb);
 
             unsigned t_fact_size = t.m_fact_size;
 
             sparse_table_plugin & plugin = t.get_plugin();
-            sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
+            sparse_table * res = get(plugin.mk_empty(get_result_signature()));
 
             const sparse_table::column_layout & src_layout = t.m_column_layout;
             const sparse_table::column_layout & tgt_layout = res->m_column_layout;
@@ -970,10 +988,11 @@ namespace datalog {
         }
 
         virtual table_base * operator()(const table_base & tb) {
-            const sparse_table & t = static_cast<const sparse_table &>(tb);
+            verbose_action  _va("select_equal_and_project");
+            const sparse_table & t = get(tb);
 
             sparse_table_plugin & plugin = t.get_plugin();
-            sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
+            sparse_table * res = get(plugin.mk_empty(get_result_signature()));
 
             const sparse_table::column_layout & t_layout = t.m_column_layout;
             const sparse_table::column_layout & res_layout = res->m_column_layout;
@@ -1056,13 +1075,14 @@ namespace datalog {
         }
 
         virtual table_base * operator()(const table_base & tb) {
+            verbose_action  _va("rename");
 
-            const sparse_table & t = static_cast<const sparse_table &>(tb);
+            const sparse_table & t = get(tb);
 
             unsigned t_fact_size = t.m_fact_size;
 
             sparse_table_plugin & plugin = t.get_plugin();
-            sparse_table * res = static_cast<sparse_table *>(plugin.mk_empty(get_result_signature()));
+            sparse_table * res = get(plugin.mk_empty(get_result_signature()));
 
             size_t res_fact_size = res->m_fact_size;
             size_t res_data_size = res_fact_size*t.row_count();
@@ -1112,17 +1132,18 @@ namespace datalog {
            If tgt_is_first is false, contains the same items as \c res.
         */
         idx_set m_intersection_content;
+        
 
     public:
         negation_filter_fn(const table_base & tgt, const table_base & neg, 
                     unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * negated_cols) 
                 : convenient_table_negation_filter_fn(tgt, neg, joined_col_cnt, t_cols, negated_cols) {
-            unsigned neg_fisrt_func = neg.get_signature().first_functional();
+            unsigned neg_first_func = neg.get_signature().first_functional();
             counter ctr;
             ctr.count(m_cols2);
             m_joining_neg_non_functional = ctr.get_max_counter_value() == 1
-                && ctr.get_positive_count() == neg_fisrt_func 
-                && (neg_fisrt_func == 0 || ctr.get_max_positive() == neg_fisrt_func-1);
+                && ctr.get_positive_count() == neg_first_func 
+                && (neg_first_func == 0 || ctr.get_max_positive() == neg_first_func-1);
         }
 
         /**
@@ -1133,9 +1154,7 @@ namespace datalog {
                 bool tgt_is_first, svector<store_offset> & res) {
             SASSERT(res.empty());
 
-            if (!tgt_is_first) {
-                m_intersection_content.reset();
-            }
+            m_intersection_content.reset();
 
             unsigned joined_col_cnt = m_cols1.size();
             unsigned t1_entry_size = t1.m_data.entry_size();
@@ -1194,8 +1213,10 @@ namespace datalog {
         }
 
         virtual void operator()(table_base & tgt0, const table_base & neg0) {
-            sparse_table & tgt = static_cast<sparse_table &>(tgt0);
-            const sparse_table & neg = static_cast<const sparse_table &>(neg0);
+            sparse_table & tgt = get(tgt0);
+            const sparse_table & neg = get(neg0);
+           
+            verbose_action  _va("filter_by_negation");
 
             if (m_cols1.size() == 0) {
                 if (!neg.empty()) {
@@ -1215,12 +1236,9 @@ namespace datalog {
                 collect_intersection_offsets(tgt, neg, true, to_remove);
             }
 
-            if (to_remove.empty()) {
-                return;
-            }
 
             //the largest offsets are at the end, so we can remove them one by one
-            while(!to_remove.empty()) {
+            while (!to_remove.empty()) {
                 store_offset removed_ofs = to_remove.back();
                 to_remove.pop_back();
                 tgt.m_data.remove_offset(removed_ofs);
@@ -1241,6 +1259,148 @@ namespace datalog {
         return alloc(negation_filter_fn, t, negated_obj, joined_col_cnt, t_cols, negated_cols);
     }
 
+    /**
+           T \ (S1 Join S2)
+
+           t_cols    - columns from T
+           s_cols    - columns from (S1 Join S2) that are equated
+           src1_cols - columns from S1 equated with columns from S2
+           src2_cols - columns from S2 equated with columns from S1
+
+           t1_cols    - columns from T that map into S1
+           s1_cols    - matching columns from s_cols for t1_cols
+           t2s1_cols  - columns from T that map into S2, and columns from src1 that join src2
+           s2_cols    - matching columns from t2s1_cols
+
+           columns from s2 that are equal to a column from s1 that is in s_cols:
+
+           - ...
+           
+    */
+
+    class sparse_table_plugin::negated_join_fn : public table_intersection_join_filter_fn {
+        typedef sparse_table::store_offset store_offset;
+        typedef sparse_table::key_value key_value;
+        typedef sparse_table::key_indexer key_indexer;
+        unsigned_vector m_t1_cols;
+        unsigned_vector m_s1_cols;
+        unsigned_vector m_t2_cols;
+        unsigned_vector m_s2_cols;
+        unsigned_vector m_src1_cols;
+    public:
+        negated_join_fn(        
+            table_base const& src1,
+            unsigned_vector const& t_cols,
+            unsigned_vector const& src_cols,
+            unsigned_vector const& src1_cols,
+            unsigned_vector const& src2_cols):
+            m_src1_cols(src1_cols) {
+
+            // split t_cols and src_cols according to src1, and src2
+
+            unsigned src1_size = src1.get_signature().size();
+            for (unsigned i = 0; i < t_cols.size(); ++i) {
+                if (src_cols[i] < src1_size) {
+                    m_t1_cols.push_back(t_cols[i]);
+                    m_s1_cols.push_back(src_cols[i]);
+                }
+                else {
+                    m_t2_cols.push_back(t_cols[i]);
+                    m_s2_cols.push_back(src_cols[i]);                    
+                }
+            }
+            m_s2_cols.append(src2_cols);
+        }
+
+        virtual void operator()(table_base & _t, const table_base & _s1, const table_base& _s2) {
+
+            verbose_action  _va("negated_join");
+            sparse_table& t = get(_t);
+            svector<store_offset> to_remove;
+            collect_to_remove(t, get(_s1), get(_s2), to_remove);
+            for (unsigned i = 0; i < to_remove.size(); ++i) {
+                t.m_data.remove_offset(to_remove[i]);
+            }
+            t.reset_indexes();
+        }
+
+    private:
+        void collect_to_remove(sparse_table& t, sparse_table const& s1, sparse_table const& s2, svector<store_offset>& to_remove) {
+            key_value s1_key, s2_key;
+            SASSERT(&s1 != &s2);
+            SASSERT(m_s1_cols.size() == m_t1_cols.size());
+            SASSERT(m_s2_cols.size() == m_t2_cols.size() + m_src1_cols.size());
+            s1_key.resize(m_s1_cols.size());
+            s2_key.resize(m_s2_cols.size());
+            key_indexer & s1_indexer = s1.get_key_indexer(m_s1_cols.size(), m_s1_cols.c_ptr());
+            key_indexer & s2_indexer = s2.get_key_indexer(m_s2_cols.size(), m_s2_cols.c_ptr());
+
+            store_offset t_after_last = t.m_data.after_last_offset();
+            key_indexer::query_result s1_offsets, s2_offsets;
+            unsigned t_entry_size = t.m_data.entry_size();
+            for (store_offset t_ofs = 0; t_ofs < t_after_last; t_ofs += t_entry_size) {
+
+                if (update_key(s1_key, 0, t, t_ofs, m_t1_cols)) {
+                    s1_offsets = s1_indexer.get_matching_offsets(s1_key);
+                }
+                key_indexer::offset_iterator it  = s1_offsets.begin();
+                key_indexer::offset_iterator end = s1_offsets.end();
+                for (; it != end; ++it) {
+                    store_offset s1_ofs = *it;
+                    bool upd1 = update_key(s2_key, 0, t, t_ofs, m_t2_cols);
+                    bool upd2 = update_key(s2_key, m_t2_cols.size(), s1, s1_ofs, m_src1_cols);
+                    if (upd1 || upd2) {
+                        s2_offsets = s2_indexer.get_matching_offsets(s2_key);
+                    }
+                    if (!s2_offsets.empty()) {
+                        to_remove.push_back(t_ofs);
+                        break;
+                    }
+                }                
+            }                       
+        }
+
+        inline bool update_key(key_value& key, unsigned key_offset, sparse_table const& t, store_offset ofs, unsigned_vector const& cols) {
+            bool modified = false;
+            unsigned sz = cols.size();
+            for (unsigned i = 0; i < sz; ++i) {
+                table_element val = t.get_cell(ofs, cols[i]);
+                modified = update_key(key[i+key_offset], val) || modified;
+            }
+            return modified;
+        }
+
+        inline bool update_key(table_element& tgt, table_element src) {
+            if (tgt == src) {
+                return false;
+            }
+            else {
+                tgt = src;
+                return true;
+            }
+        }
+        
+    };
+
+    table_intersection_join_filter_fn* sparse_table_plugin::mk_filter_by_negated_join_fn(
+        const table_base & t, 
+
+
+        const table_base & src1, 
+        const table_base & src2, 
+        unsigned_vector const& t_cols,
+        unsigned_vector const& src_cols,
+        unsigned_vector const& src1_cols,
+        unsigned_vector const& src2_cols) {
+        if (check_kind(t) && check_kind(src1) && check_kind(src2)) {            
+            return alloc(negated_join_fn, src1, t_cols, src_cols, src1_cols, src2_cols);
+        }
+        else {
+            return 0;
+        }
+    }
+
+
     unsigned sparse_table::get_size_estimate_bytes() const {
         unsigned sz = 0;
         sz += m_data.get_size_estimate_bytes();
diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h
index 0a60c4e10..0222aa6e2 100644
--- a/src/muz/rel/dl_sparse_table.h
+++ b/src/muz/rel/dl_sparse_table.h
@@ -48,6 +48,7 @@ namespace datalog {
         class project_fn;
         class negation_filter_fn;
         class select_equal_and_project_fn;
+        class negated_join_fn;
 
         typedef ptr_vector<sparse_table> sp_table_vector;
         typedef map<table_signature, sp_table_vector *, 
@@ -93,6 +94,20 @@ namespace datalog {
         virtual table_intersection_filter_fn * mk_filter_by_negation_fn(const table_base & t, 
                 const table_base & negated_obj, unsigned joined_col_cnt, 
                 const unsigned * t_cols, const unsigned * negated_cols);
+        virtual table_intersection_join_filter_fn* mk_filter_by_negated_join_fn(
+            const table_base & t, 
+            const table_base & src1, 
+            const table_base & src2, 
+            unsigned_vector const& t_cols,
+            unsigned_vector const& src_cols,
+            unsigned_vector const& src1_cols,
+            unsigned_vector const& src2_cols);
+
+        static sparse_table const& get(table_base const&);
+        static sparse_table& get(table_base&);
+        static sparse_table const* get(table_base const*);
+        static sparse_table* get(table_base*);
+
     };
 
     class entry_storage {
diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp
index 3c30c58bb..364c29367 100644
--- a/src/muz/rel/dl_table_relation.cpp
+++ b/src/muz/rel/dl_table_relation.cpp
@@ -39,16 +39,15 @@ namespace datalog {
 
     bool table_relation_plugin::can_handle_signature(const relation_signature & s) {
         table_signature tsig;
-        if(!get_manager().relation_signature_to_table(s, tsig)) {
-            return false;
-        }
-        return m_table_plugin.can_handle_signature(tsig);
+        return 
+            get_manager().relation_signature_to_table(s, tsig) &&
+            m_table_plugin.can_handle_signature(tsig);
     }
 
 
     relation_base * table_relation_plugin::mk_empty(const relation_signature & s) {
         table_signature tsig;
-        if(!get_manager().relation_signature_to_table(s, tsig)) {
+        if (!get_manager().relation_signature_to_table(s, tsig)) {
             return 0;
         }
         table_base * t = m_table_plugin.mk_empty(tsig);
@@ -92,6 +91,7 @@ namespace datalog {
 
             TRACE("dl_table_relation", tout << "# join => "; tres->display(tout););
             if(&tres->get_plugin()!=&plugin.m_table_plugin) {
+                IF_VERBOSE(1, verbose_stream() << "new type returned\n";);
                 //Operation returned a table of different type than the one which is associated with
                 //this plugin. We need to get a correct table_relation_plugin and create the relation 
                 //using it.
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index c57ef2606..b44f67644 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -31,6 +31,7 @@ Revision History:
 #include"dl_interval_relation.h"
 #include"karr_relation.h"
 #include"dl_finite_product_relation.h"
+#include"dl_lazy_table.h"
 #include"dl_sparse_table.h"
 #include"dl_table.h"
 #include"dl_table_relation.h"
@@ -45,6 +46,7 @@ Revision History:
 #include"dl_mk_rule_inliner.h"
 #include"dl_mk_interp_tail_simplifier.h"
 #include"dl_mk_bit_blast.h"
+#include"fixedpoint_params.hpp"
 
 
 namespace datalog {
@@ -96,17 +98,19 @@ namespace datalog {
 
         // register plugins for builtin tables
 
-        get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
+        relation_manager& rm = get_rmanager();
 
+        rm.register_plugin(alloc(sparse_table_plugin, rm));
+        rm.register_plugin(alloc(hashtable_table_plugin, rm));
+        rm.register_plugin(alloc(bitvector_table_plugin, rm));
+        rm.register_plugin(alloc(equivalence_table_plugin, rm));
+        rm.register_plugin(lazy_table_plugin::mk_sparse(rm));
 
         // register plugins for builtin relations
 
-        get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(karr_relation_plugin, get_rmanager()));
+        rm.register_plugin(alloc(bound_relation_plugin, rm));
+        rm.register_plugin(alloc(interval_relation_plugin, rm));
+        rm.register_plugin(alloc(karr_relation_plugin, rm));
     }
 
     rel_context::~rel_context() {
diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp
index 2201be73e..83842a68b 100644
--- a/src/muz/tab/tab_context.cpp
+++ b/src/muz/tab/tab_context.cpp
@@ -30,6 +30,7 @@ Revision History:
 #include "for_each_expr.h"
 #include "matcher.h"
 #include "scoped_proof.h"
+#include "fixedpoint_params.hpp"
 
 namespace tb {
 
diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index 271003fff..08f295ff4 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -24,6 +24,7 @@ Revision History:
 #include "expr_safe_replace.h"
 #include "filter_model_converter.h"
 #include "dl_mk_interp_tail_simplifier.h"
+#include "fixedpoint_params.hpp"
 
 namespace datalog {
 
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index 8583fbe45..31af7a53f 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -52,14 +52,10 @@ namespace datalog {
         ptr_vector<func_decl> todo;
         rule_set::decl2rules body2rules;
         // initialization for reachability
-            rel_context_base* rc = m_context.get_rel_context();
         for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
             rule * r = *it;
             all.insert(r->get_decl());
-            bool non_empty = 
-                (rc && !rc->is_empty_relation(r->get_decl())) ||
-                r->get_uninterpreted_tail_size() == 0;
-            if (non_empty) {
+            if (r->get_uninterpreted_tail_size() == 0) {
                 if (!reached.contains(r->get_decl())) {
                     reached.insert(r->get_decl());
                     todo.insert(r->get_decl());
@@ -77,6 +73,17 @@ namespace datalog {
                 }
             }
         }
+        rel_context_base* rc = m_context.get_rel_context();
+        if (rc) {
+            func_decl_set::iterator fit = all.begin(), fend = all.end();
+            for (; fit != fend; ++fit) {
+                if (!rc->is_empty_relation(*fit) &&
+                    !reached.contains(*fit)) {
+                    reached.insert(*fit);
+                    todo.insert(*fit);
+                }
+            }                 
+        }
         // reachability computation
         while (!todo.empty()) {
             func_decl * d = todo.back();
diff --git a/src/muz/transforms/dl_mk_karr_invariants.cpp b/src/muz/transforms/dl_mk_karr_invariants.cpp
index 4c0a24b65..b4ab66bc2 100644
--- a/src/muz/transforms/dl_mk_karr_invariants.cpp
+++ b/src/muz/transforms/dl_mk_karr_invariants.cpp
@@ -39,6 +39,7 @@ Revision History:
 #include"dl_mk_karr_invariants.h"
 #include"dl_mk_backwards.h"
 #include"dl_mk_loop_counter.h"
+#include"fixedpoint_params.hpp"
 
 namespace datalog {
 
diff --git a/src/muz/transforms/dl_mk_magic_symbolic.cpp b/src/muz/transforms/dl_mk_magic_symbolic.cpp
index a06a573ad..57490466c 100644
--- a/src/muz/transforms/dl_mk_magic_symbolic.cpp
+++ b/src/muz/transforms/dl_mk_magic_symbolic.cpp
@@ -54,6 +54,7 @@ Revision History:
 
 #include"dl_mk_magic_symbolic.h"
 #include"dl_context.h"
+#include"fixedpoint_params.hpp"
 
 namespace datalog {
 
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
index 68f5bc3a3..e686495e9 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
@@ -23,6 +23,8 @@ Revision History:
 #include "dl_context.h"
 #include "expr_safe_replace.h"
 #include "expr_abstract.h"
+#include"fixedpoint_params.hpp"
+
 
 namespace datalog {
 
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index b24e3e81c..ebb9310a4 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -26,6 +26,8 @@ Revision History:
 #include "dl_mk_quantifier_instantiation.h"
 #include "dl_context.h"
 #include "pattern_inference.h"
+#include "fixedpoint_params.hpp"
+
 
 namespace datalog {
 
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index 65ce44b8b..3e933b099 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -52,6 +52,7 @@ Subsumption transformation (remove rule):
 #include "rewriter.h"
 #include "rewriter_def.h"
 #include "dl_mk_rule_inliner.h"
+#include "fixedpoint_params.hpp"
 
 namespace datalog {
 
diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp
index d666d0ca8..9618db88e 100644
--- a/src/muz/transforms/dl_mk_scale.cpp
+++ b/src/muz/transforms/dl_mk_scale.cpp
@@ -18,6 +18,7 @@ Revision History:
 
 #include"dl_mk_scale.h"
 #include"dl_context.h"
+#include"fixedpoint_params.hpp"
 
 namespace datalog {
 
diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp
index 7c5707ccf..2cf48d46b 100644
--- a/src/muz/transforms/dl_transforms.cpp
+++ b/src/muz/transforms/dl_transforms.cpp
@@ -33,6 +33,7 @@ Revision History:
 #include"dl_mk_quantifier_instantiation.h"
 #include"dl_mk_subsumption_checker.h"
 #include"dl_mk_scale.h"
+#include"fixedpoint_params.hpp"
 
 namespace datalog {
 
diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp
index 15681ea36..a487a99b4 100644
--- a/src/shell/datalog_frontend.cpp
+++ b/src/shell/datalog_frontend.cpp
@@ -232,10 +232,9 @@ unsigned read_datalog(char const * file) {
         TRACE("dl_compiler", ctx.display(tout);
               rules_code.display(*ctx.get_rel_context(), tout););
         
-        if (ctx.get_params().output_tuples()) {
+        if (ctx.output_tuples()) {
             ctx.get_rel_context()->display_output_facts(ctx.get_rules(), std::cout);
         }
-
         display_statistics(
             std::cout,
             ctx,