diff --git a/lib/dl_bmc_engine.cpp b/lib/dl_bmc_engine.cpp
index 8ad46ae3e..1ff04196d 100644
--- a/lib/dl_bmc_engine.cpp
+++ b/lib/dl_bmc_engine.cpp
@@ -97,9 +97,9 @@ namespace datalog {
             return check_linear();
         }
         else {
+            check_nonlinear();
             IF_VERBOSE(1, verbose_stream() << "non-linear BMC is not supported\n";);
             return l_undef;
-            return check_nonlinear();
         }
     }
 
@@ -640,14 +640,19 @@ namespace datalog {
     lbool bmc::check_query() {
         sort* trace_sort = m_pred2sort.find(m_query_pred);
         func_decl_ref q = mk_predicate(m_query_pred);
-        assert_expr(m.mk_app(q, m.mk_const(symbol("trace"), trace_sort), m.mk_const(symbol("path"),m_path_sort)));
+        expr_ref trace(m), path(m);
+        trace = m.mk_const(symbol("trace"), trace_sort);
+        path  = m.mk_const(symbol("path"),m_path_sort);
+        assert_expr(m.mk_app(q, trace, path));
         lbool is_sat = m_solver.check();
         if (is_sat == l_undef) {
             model_ref md;
             proof_ref pr(m);
             m_solver.get_model(md);
             IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0););
-            
+            md->eval(trace, trace);
+            IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n";);
+            IF_VERBOSE(2, m_solver.display(verbose_stream()););
         }
         return is_sat;
     }
diff --git a/lib/dl_check_table.cpp b/lib/dl_check_table.cpp
index de3a71746..1b1dd4974 100644
--- a/lib/dl_check_table.cpp
+++ b/lib/dl_check_table.cpp
@@ -48,6 +48,7 @@ namespace datalog {
      table_base const* check_table_plugin::tocheck(table_base const* r) { return r?(get(*r).m_tocheck):0; }
 
     table_base * check_table_plugin::mk_empty(const table_signature & s) {
+        IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
         table_base* checker = m_checker.mk_empty(s);
         table_base* tocheck = m_tocheck.mk_empty(s);
         return alloc(check_table, *this, s, tocheck, checker);
@@ -65,9 +66,11 @@ namespace datalog {
         }
 
         virtual table_base* operator()(const table_base & t1, const table_base & t2) {
+            IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
             table_base* ttocheck = (*m_tocheck)(tocheck(t1), tocheck(t2));
             table_base* tchecker = (*m_checker)(checker(t1), checker(t2));
-            return alloc(check_table, get(t1).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
+            check_table* result = alloc(check_table, get(t1).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
+            return result;
         }
     };
 
@@ -89,9 +92,10 @@ namespace datalog {
         }
         
         virtual void operator()(table_base& tgt, const table_base& src, table_base* delta) {
+            IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
             (*m_tocheck)(tocheck(tgt), tocheck(src), tocheck(delta));
             (*m_checker)(checker(tgt), checker(src), checker(delta));
-            SASSERT(get(tgt).well_formed());
+            get(tgt).well_formed();
         }
     };
 
@@ -113,9 +117,11 @@ namespace datalog {
         }
 
         table_base* operator()(table_base const& src) {
+            IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
             table_base* tchecker = (*m_checker)(checker(src));
             table_base* ttocheck = (*m_tocheck)(tocheck(src));
-            return alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker);
+            check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker);
+            return result;
         }
     };
     
@@ -136,9 +142,11 @@ namespace datalog {
         }
 
         table_base* operator()(table_base const& src) {
+            IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
             table_base* tchecker = (*m_checker)(checker(src));
             table_base* ttocheck = (*m_tocheck)(tocheck(src));
-            return alloc(check_table, get(src).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
+            check_table* result = alloc(check_table, get(src).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
+            return result;
         }
     };
     
@@ -162,7 +170,7 @@ namespace datalog {
         void operator()(table_base & t) {
             (*m_checker)(checker(t));
             (*m_tocheck)(tocheck(t));
-            SASSERT(get(t).well_formed());
+            get(t).well_formed();
         }
     };
 
@@ -187,7 +195,7 @@ namespace datalog {
         virtual void operator()(table_base& src) {
             (*m_checker)(checker(src));
             (*m_tocheck)(tocheck(src));
-            SASSERT(get(src).well_formed());
+            get(src).well_formed();
         }
     };
 
@@ -211,7 +219,7 @@ namespace datalog {
         virtual void operator()(table_base& src) {
             (*m_checker)(checker(src));
             (*m_tocheck)(tocheck(src));
-            SASSERT(get(src).well_formed());
+            get(src).well_formed();
         }
     };
 
@@ -236,9 +244,10 @@ namespace datalog {
         }
 
         virtual void operator()(table_base& src, table_base const& negated_obj) {
+            IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
             (*m_checker)(checker(src), checker(negated_obj));
             (*m_tocheck)(tocheck(src), tocheck(negated_obj));
-            SASSERT(get(src).well_formed());
+            get(src).well_formed();
         }
         
     };
@@ -258,14 +267,14 @@ namespace datalog {
 
     check_table::check_table(check_table_plugin & p, const table_signature & sig):
         table_base(p, sig) {
-        SASSERT(well_formed());
+        (well_formed());
     }
 
     check_table::check_table(check_table_plugin & p, const table_signature & sig, table_base* tocheck, table_base* checker):
         table_base(p, sig),
         m_checker(checker),
         m_tocheck(tocheck) {            
-        SASSERT(well_formed());
+        well_formed();
     }
 
     check_table::~check_table() {
@@ -274,6 +283,10 @@ namespace datalog {
     }
 
     bool check_table::well_formed() const {
+        get_plugin().m_count++;
+        if (get_plugin().m_count == 497) {
+            std::cout << "here\n";
+        }
         iterator it = m_tocheck->begin(), end = m_tocheck->end();
         for (; it != end; ++it) {
             table_fact fact;
@@ -281,7 +294,9 @@ namespace datalog {
             if (!m_checker->contains_fact(fact)) {
                 m_tocheck->display(verbose_stream());
                 m_checker->display(verbose_stream());
+                verbose_stream() << get_plugin().m_count << "\n";
                 UNREACHABLE();
+                fatal_error(0);
                 return false;
             }
         }
@@ -292,7 +307,9 @@ namespace datalog {
             if (!m_tocheck->contains_fact(fact)) {
                 m_tocheck->display(verbose_stream());
                 m_checker->display(verbose_stream());
+                verbose_stream() << get_plugin().m_count << "\n";
                 UNREACHABLE();
+                fatal_error(0);
                 return false;
             }
         }
@@ -300,20 +317,28 @@ namespace datalog {
     }
 
     bool check_table::empty() const {
+        if (m_tocheck->empty() != m_checker->empty()) {
+            m_tocheck->display(verbose_stream());
+            m_checker->display(verbose_stream());
+            verbose_stream() << get_plugin().m_count << "\n";
+            fatal_error(0);
+        }
         return m_tocheck->empty();
     }
 
 
     void check_table::add_fact(const table_fact & f) {
+        IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
         m_tocheck->add_fact(f);
         m_checker->add_fact(f);
-        SASSERT(well_formed());        
+        well_formed();        
     }
 
     void check_table::remove_fact(const table_element*  f) {
+        IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
         m_tocheck->remove_fact(f);
         m_checker->remove_fact(f);
-        SASSERT(well_formed());        
+        well_formed();        
     }
 
     bool check_table::contains_fact(const table_fact & f) const {
@@ -321,11 +346,14 @@ namespace datalog {
     }
     
     table_base * check_table::clone() const {        
-        return alloc(check_table, get_plugin(), get_signature(), m_tocheck->clone(), m_checker->clone());
+        IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
+        check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->clone(), m_checker->clone());
+        return result;
     }
 
     table_base * check_table::complement(func_decl* p) const {
-        return alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p), m_checker->complement(p));
+        check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p), m_checker->complement(p));
+        return result;
     }
 
 };
diff --git a/lib/dl_check_table.h b/lib/dl_check_table.h
index 1c7490cda..6f098f8bc 100644
--- a/lib/dl_check_table.h
+++ b/lib/dl_check_table.h
@@ -32,6 +32,7 @@ namespace datalog {
         friend class check_table;
         table_plugin& m_checker;
         table_plugin& m_tocheck;
+        unsigned m_count;
     protected:
         class join_fn;
         class union_fn;
@@ -47,7 +48,7 @@ namespace datalog {
         check_table_plugin(relation_manager & manager, symbol const& checker, symbol const& tocheck) 
             : table_plugin(symbol("check"), manager),
             m_checker(*manager.get_table_plugin(checker)),
-            m_tocheck(*manager.get_table_plugin(tocheck)) {}
+            m_tocheck(*manager.get_table_plugin(tocheck)), m_count(0) {}
 
         virtual table_base * mk_empty(const table_signature & s);
 
diff --git a/lib/dl_context.cpp b/lib/dl_context.cpp
index 079fcaa9e..b64bf3925 100644
--- a/lib/dl_context.cpp
+++ b/lib/dl_context.cpp
@@ -1214,9 +1214,8 @@ namespace datalog {
 
     lbool context::pdr_query(expr* query) {
         ensure_pdr();
-        lbool result  = m_pdr->query(query);
-        m_last_answer = m_pdr->get_answer();
-        return result;
+        m_last_answer = 0; 
+        return m_pdr->query(query);
     }
 
     void context::ensure_bmc() {
@@ -1227,9 +1226,8 @@ namespace datalog {
 
     lbool context::bmc_query(expr* query) {
         ensure_bmc();
-        lbool result = m_bmc->query(query);
-        m_last_answer = m_bmc->get_answer();
-        return result;
+        m_last_answer = 0;
+        return m_bmc->query(query);
     }
 
 #define BEGIN_QUERY()                           \
@@ -1442,6 +1440,23 @@ namespace datalog {
     }
     
     expr* context::get_answer_as_formula() {
+        if (m_last_answer) {
+            return m_last_answer.get();
+        }
+        switch(get_engine()) {
+        case PDR_ENGINE: 
+        case QPDR_ENGINE:
+            ensure_pdr();
+            m_last_answer = m_pdr->get_answer();
+            return m_last_answer.get();
+        case BMC_ENGINE:
+            ensure_bmc();
+            m_last_answer = m_bmc->get_answer();
+            return m_last_answer.get();
+        default:
+            UNREACHABLE();
+        }
+        m_last_answer = m.mk_false();
         return m_last_answer.get();
     }
 
diff --git a/lib/dl_skip_table.cpp b/lib/dl_skip_table.cpp
index 50786e22b..28efaabee 100644
--- a/lib/dl_skip_table.cpp
+++ b/lib/dl_skip_table.cpp
@@ -215,7 +215,9 @@ namespace datalog {
                 col2 = m_cycle[0];
                 swap2(n, col1, col2);
             }
-            return alloc(skip_table, s.get_plugin(), get_result_signature(), n);
+            skip_table* res = alloc(skip_table, s.get_plugin(), get_result_signature(), n);
+            TRACE("skip",res->display(tout););
+            return res;
         }
     };
     
diff --git a/lib/dl_util.cpp b/lib/dl_util.cpp
index 57be631c2..574b80599 100644
--- a/lib/dl_util.cpp
+++ b/lib/dl_util.cpp
@@ -605,6 +605,12 @@ namespace datalog {
                     body.push_back(r.get_tail(i));
                 }
             }
+            TRACE("dl_dr", 
+                  tout << r.get_decl()->get_name() << "\n";
+                  for (unsigned i = 0; i < body.size(); ++i) {
+                      tout << mk_pp(body[i].get(), m) << "\n";
+                  });
+                      
             mc->insert(r.get_head(), body.size(), body.c_ptr());
         }
     }
diff --git a/lib/horn_subsume_model_converter.cpp b/lib/horn_subsume_model_converter.cpp
index b2b76e39c..83061ca6f 100644
--- a/lib/horn_subsume_model_converter.cpp
+++ b/lib/horn_subsume_model_converter.cpp
@@ -23,6 +23,7 @@ Revision History:
 #include "ast_pp.h"
 #include "model_smt2_pp.h"
 #include "bool_rewriter.h"
+#include "th_rewriter.h"
 
 void horn_subsume_model_converter::insert(app* head, expr* body) {
     func_decl_ref pred(m);
@@ -174,19 +175,49 @@ bool horn_subsume_model_converter::mk_horn(
     }
 }
 
+void horn_subsume_model_converter::add_default_proc::operator()(app* n) {
+    //
+    // predicates that have not been assigned values 
+    // in the Horn model are assumed false.
+    //
+    if (m.is_bool(n) && 
+        !m_md->has_interpretation(n->get_decl()) &&
+        (n->get_family_id() == null_family_id)) {
+        TRACE("dl_mc", tout << "adding: " << n->get_decl()->get_name() << "\n";);
+        if (n->get_decl()->get_arity() == 0) {
+            m_md->register_decl(n->get_decl(), m.mk_false());
+        }
+        else { 
+            func_interp* fi = alloc(func_interp, m, n->get_decl()->get_arity());
+            fi->set_else(m.mk_false());
+            m_md->register_decl(n->get_decl(), fi);            
+        }
+    }
+}
+
+void horn_subsume_model_converter::add_default_false_interpretation(expr* e, model_ref& md) {
+    add_default_proc proc(m, md);
+    for_each_expr(proc, e);
+}
+
 
 void horn_subsume_model_converter::operator()(model_ref& mr) {
+    TRACE("dl_mc", model_smt2_pp(tout, m, *mr, 0););
     for (unsigned i = m_funcs.size(); i > 0; ) {
         --i;
         func_decl* h = m_funcs[i].get();
         expr_ref body(m_bodies[i].get(), m);
         unsigned arity = h->get_arity();
-        
+        add_default_false_interpretation(body, mr);
+                
+        TRACE("dl_mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";);
         expr_ref tmp(body);
         mr->eval(tmp, body);
-        TRACE("dl", tout << "eval: " << mk_pp(tmp, m) << "\nto:\n" << mk_pp(body, m) << "\n";);
-        TRACE("dl", model_smt2_pp(tout, m, *mr, 0););
+        th_rewriter rw(m);
+        rw(body);
         
+        TRACE("dl_mc", tout << "to:\n" << mk_pp(body, m) << "\n";);
+                
         if (arity == 0) {
             expr* e = mr->get_const_interp(h);
             if (e) {
diff --git a/lib/horn_subsume_model_converter.h b/lib/horn_subsume_model_converter.h
index 91172a72c..5a1ca6df9 100644
--- a/lib/horn_subsume_model_converter.h
+++ b/lib/horn_subsume_model_converter.h
@@ -42,6 +42,16 @@ class horn_subsume_model_converter : public model_converter {
     func_decl_ref_vector m_funcs;
     expr_ref_vector      m_bodies;
 
+    void add_default_false_interpretation(expr* e, model_ref& md);
+
+    struct add_default_proc {
+        ast_manager& m;
+        model_ref& m_md;
+        add_default_proc(ast_manager& m, model_ref& md): m(m), m_md(md) {}
+        void operator()(app* n);
+        void operator()(expr* n) {}
+    };
+
 public:
 
     horn_subsume_model_converter(ast_manager& m): m(m), m_funcs(m), m_bodies(m) {}
diff --git a/lib/imdd.cpp b/lib/imdd.cpp
index 159863625..c8efca67a 100644
--- a/lib/imdd.cpp
+++ b/lib/imdd.cpp
@@ -255,6 +255,7 @@ void imdd_manager::mark_as_dead(imdd * d) {
 
 void imdd_manager::deallocate_imdd(imdd * d) { 
     SASSERT(d->is_dead());
+    memset(d, 0, sizeof(*d));
     m_alloc.deallocate(sizeof(imdd), d); 
 }
 
@@ -724,7 +725,7 @@ imdd * imdd_manager::mk_union_core(imdd * d1, imdd * d2, bool destructive, bool
 
                 if (head1 < head2) {
                     it1.move_to(head2);
-                    head1 = it1 != end1 ? it1->begin_key() : UINT_MAX;
+                    head1 = it1 != end1 ? (it1->begin_key() < head2?head2:it1->begin_key()): UINT_MAX;
                 }
                 else if (head1 > head2) {
                     copy_upto(head2, it2, end2, head1, to_insert);
@@ -1635,7 +1636,8 @@ imdd* imdd_manager::filter_identical_loop3(imdd * d, unsigned v1, bool del1, uns
 }
 
 void imdd_manager::merge_intervals(svector<interval>& dst, svector<interval> const& src) {
-    svector<interval> tmp;
+    svector<interval>& tmp = m_i_nodes_tmp;
+    tmp.reset();
     // invariant: intervals are sorted.
     for (unsigned i = 0, j = 0; i < src.size() || j < dst.size();) {
         SASSERT(!(i + 1 < src.size()) || src[i].m_hi < src[i+1].m_lo);
@@ -1685,8 +1687,8 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
     // For each level up to 'v' create a list of nodes visited
     // insert to a map the set of intervals that visit the node.
     // 
-    filter_id_map nodes;
-    filter_id_map::obj_map_entry* e;
+    m_nodes.reset();
+    filter_id_map& nodes = m_nodes;
     imdd* d1, *d2, *d3;
     vector<ptr_vector<imdd> > levels;
     levels.push_back(ptr_vector<imdd>());
@@ -1696,24 +1698,23 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
     imdd* curr_child;
     for (; it != end; ++it) {
         curr_child = it->val();
-        e = nodes.insert_if_not_there2(curr_child, svector<interval>());
-        if (e->get_data().m_value.empty()) {
+        svector<interval>& iv = nodes.init(curr_child);
+        if (iv.empty()) {
             levels.back().push_back(curr_child);
         }
-        e->get_data().m_value.push_back(interval(it->begin_key(), it->end_key()));        
+        iv.push_back(interval(it->begin_key(), it->end_key()));        
     }
 
     for (unsigned j = 0; j+1 < v; ++j) {
         levels.push_back(ptr_vector<imdd>());        
         for (unsigned i = 0; i < levels[j].size(); ++i) {
             d1 = levels[j][i];
-            svector<interval> i_nodes = nodes.find(d1);
+            svector<interval>& i_nodes = nodes.init(d1);
             it  = d1->begin_children();
             end = d1->end_children();
             for(; it != end; ++it) {
                 imdd* curr_child = it->val();
-                e = nodes.insert_if_not_there2(curr_child, svector<interval>());
-                svector<interval>& i_nodes2 = e->get_data().m_value;
+                svector<interval>& i_nodes2 = nodes.init(curr_child);
                 if (i_nodes2.empty()) {
                     levels[j+1].push_back(curr_child);
                     i_nodes2.append(i_nodes);
@@ -1730,7 +1731,7 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
               tout << "Level: " << i << "\n";
               for (unsigned j = 0; j < levels[i].size(); ++j) {
                   tout << levels[i][j]->get_id() << " ";
-                  svector<interval> const& i_nodes = nodes.find(levels[i][j]);
+                  svector<interval> const& i_nodes = nodes.init(levels[i][j]);
                   for (unsigned k = 0; k < i_nodes.size(); ++k) {
                       tout << i_nodes[k].m_lo << ":" << i_nodes[k].m_hi << " ";
                   }
@@ -1749,15 +1750,16 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
     //   => del1 & !del2:    d |-> [I |-> d'[I:ch]] // intersections of intervals.
     //
     
-    filter_idd_map nodes_dd;
+    m_nodes_dd.reset();
+    filter_idd_map& nodes_dd = m_nodes_dd;
     SASSERT(levels.size() == v);
     for (unsigned i = 0; i < levels[v-1].size(); ++i) {
         d1 = levels[v-1][i];
-        svector<interval> const & i_nodes = nodes.find(d1);
+        svector<interval> const & i_nodes = nodes.init(d1);
         it  = d1->begin_children();
         end = d1->end_children();
         unsigned j = 0;
-        svector<interval_dd> i_nodes_dd;
+        svector<interval_dd>& i_nodes_dd = nodes_dd.init(d1);
         while (it != end && j < i_nodes.size()) {
             unsigned lo1 = it->begin_key();
             unsigned hi1 = it->end_key();
@@ -1816,7 +1818,6 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
                 i_nodes_dd[k].m_dd = d2;
             }
         }
-        nodes_dd.insert(d1, i_nodes_dd);
     }    
 
     TRACE("imdd", print_filter_idd(tout, nodes_dd););  
@@ -1841,15 +1842,21 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
         --i;
         for (unsigned j = 0; j < levels[i].size(); ++j) {
             d1 = levels[i][j];
-            svector<interval_dd> i_nodes_dd;
-            svector<interval> i_nodes = nodes.find(d1);
+            m_i_nodes_dd.reset();
+            svector<interval> i_nodes = nodes.init(d1);
+            svector<interval_dd>& i_nodes_dd = nodes_dd.init(d1);
             it  = d1->begin_children();
             end = d1->end_children();
-            unsigned_vector offsets;
+            unsigned num_children = 0;
+            for( ; it != end; ++it, ++num_children);
+
+            m_offsets.reset();
+            unsigned_vector& offsets = m_offsets;
+            offsets.resize(num_children);
+            it  = d1->begin_children();
             for( ; it != end; ++it) {
                 curr_child = it->val();
-                refine_intervals(i_nodes, nodes_dd.find(curr_child));
-                offsets.push_back(0);
+                refine_intervals(i_nodes, nodes_dd.init(curr_child));
             }            
             
             for (unsigned k = 0; k < i_nodes.size(); ++k) {
@@ -1858,7 +1865,7 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
                 it = d1->begin_children();
                 for(unsigned child_id = 0; it != end; ++it, ++child_id) {
                     curr_child = it->val();
-                    svector<interval_dd> const& ch_nodes_dd = nodes_dd.find(curr_child);
+                    svector<interval_dd> const& ch_nodes_dd = nodes_dd.init(curr_child);
                     unsigned offset = offsets[child_id];
                     TRACE("imdd_verbose", tout << intv.m_lo << ":" << intv.m_hi << "\n";
                           for (unsigned l = offset; l < ch_nodes_dd.size(); ++l) {
@@ -1899,7 +1906,7 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
                 }
             }
             TRACE("imdd", tout << d1->get_id() << ": "; print_interval_dd(tout, i_nodes_dd););                           
-            nodes_dd.insert(d1, i_nodes_dd);
+            
         }
     }
 
@@ -1919,11 +1926,14 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
     it  = d->begin_children();
     end = d->end_children();
     d1  = _mk_empty(d->get_arity()-del1-del2);
-    svector<interval_dd> i_nodes_dd, i_nodes_tmp;
+    m_i_nodes_dd.reset();
+    m_i_nodes_tmp.reset();
+    svector<interval_dd>& i_nodes_dd = m_i_nodes_dd;
+    svector<interval_dd>& i_nodes_tmp = m_i_nodes_dd_tmp;
     for (; it != end; ++it) {
         curr_child = it->val();
         i_nodes_tmp.reset();
-        svector<interval_dd> const& i_nodes_dd1 = nodes_dd.find(curr_child);
+        svector<interval_dd> const& i_nodes_dd1 = nodes_dd.init(curr_child);
         for (unsigned i = 0, j = 0; i < i_nodes_dd.size() || j < i_nodes_dd1.size(); ) {
             if (i < i_nodes_dd.size() && j < i_nodes_dd1.size()) {
                 interval_dd const& iv1 = i_nodes_dd[i];
@@ -1986,9 +1996,9 @@ void imdd_manager::print_interval_dd(std::ostream& out, svector<interval_dd> con
 
 void imdd_manager::print_filter_idd(std::ostream& out, filter_idd_map const& m) {
     filter_idd_map::iterator it = m.begin(), end = m.end();
-    for (; it != end; ++it) {
-        out << it->m_key->get_id() << ": ";
-        print_interval_dd(out, it->m_value);
+    for (unsigned i = 0; it != end; ++it, ++i) {
+        out << i << ": ";
+        print_interval_dd(out, *it);
     }
 }
 
@@ -1999,12 +2009,16 @@ void imdd_manager::print_filter_idd(std::ostream& out, filter_idd_map const& m)
 */
 
 void imdd_manager::refine_intervals(svector<interval>& i_nodes, svector<interval_dd> const& i_nodes_dd) {
-    svector<interval> result;
-    for (unsigned i = 0, j = 0; i < i_nodes.size(); ++i) {
-        result.push_back(i_nodes[i]);
-        unsigned lo = result.back().m_lo;
-        unsigned hi = result.back().m_hi;
-        for (; j < i_nodes_dd.size(); ++j) {
+    m_i_nodes.reset();
+    svector<interval>& result = m_i_nodes;
+    unsigned sz1 = i_nodes.size();
+    unsigned sz2 = i_nodes_dd.size();
+    for (unsigned i = 0, j = 0; i < sz1; ++i) {
+        interval& iv = i_nodes[i];
+        result.push_back(iv);
+        unsigned lo = iv.m_lo;
+        unsigned hi = iv.m_hi;
+        for (; j < sz2; ++j) {
             unsigned lo1 = i_nodes_dd[j].m_lo;
             unsigned hi1 = i_nodes_dd[j].m_hi;
             SASSERT(lo <= hi);
@@ -2402,6 +2416,7 @@ void imdd_manager::mk_swap_acc1_dupdt(imdd_ref & d, unsigned lower, unsigned upp
     if (lower <= upper) {
         add_child(d, lower, upper, grandchild);
     }
+    TRACE("mk_swap_bug", tout << "after mk_swap_acc1_dupt\n" << mk_ll_pp(d, *this) << "\n";);
 }
 
 void imdd_manager::mk_swap_acc1(imdd * d, imdd_ref & r, unsigned lower, unsigned upper, imdd * grandchild, bool memoize_res) {
@@ -2437,6 +2452,7 @@ void imdd_manager::mk_swap_acc1(imdd * d, imdd_ref & r, unsigned lower, unsigned
     if (lower <= upper) {
         add_child(r, lower, upper, grandchild);
     }
+    TRACE("mk_swap_bug", tout << "after mk_swap_acc1\n" << mk_ll_pp(r, *this) << "\n";);
 }
 
 /**
@@ -2456,6 +2472,7 @@ void imdd_manager::mk_swap_acc2(imdd_ref & r, unsigned lower1, unsigned upper1,
     imdd_children::ext_iterator it;  
     imdd_children::ext_iterator end;
     r->m_children.move_geq(it, lower1);
+    SASSERT(m_swap_new_child == 0);    
     
     while(it != end && lower1 <= upper1) {
         imdd_children::entry const & curr_entry = *it;
@@ -2463,6 +2480,7 @@ void imdd_manager::mk_swap_acc2(imdd_ref & r, unsigned lower1, unsigned upper1,
         unsigned curr_entry_end_key   = curr_entry.end_key();
         imdd *   curr_entry_val       = curr_entry.val();
         bool     move_head            = true;
+        TRACE("mk_swap_bug", tout << lower1 << " " << upper1 << " " << curr_entry_begin_key << "\n";);
         if (upper1 < curr_entry_begin_key)
             break;
         if (lower1 < curr_entry_begin_key) {
@@ -2509,6 +2527,10 @@ void imdd_manager::mk_swap_acc2(imdd_ref & r, unsigned lower1, unsigned upper1,
         imdd * new_child = mk_swap_new_child(lower2, upper2, grandchild);            
         add_child(r, lower1, upper1, new_child);
     }
+    if (m_swap_new_child != 0) {
+        dec_ref(m_swap_new_child);
+        m_swap_new_child = 0;
+    }
     TRACE("mk_swap_bug", tout << "after mk_swap_acc2\n" << mk_ll_pp(r, *this) << "\n";);
 }
 
@@ -2562,10 +2584,7 @@ void imdd_manager::mk_swap_top_vars(imdd * d, imdd_ref & r, bool memoize_res) {
             imdd * grandchild = it2->val();
             mk_swap_acc2(r, it2->begin_key(), it2->end_key(), it->begin_key(), it->end_key(), grandchild, memoize_res);
         }
-        if (m_swap_new_child != 0) {
-            dec_ref(m_swap_new_child);
-            m_swap_new_child = 0;
-        }
+        SASSERT(m_swap_new_child == 0);
     }
 
     if (memoize_res && m_swap_granchildren_memoized) {
diff --git a/lib/imdd.h b/lib/imdd.h
index 61d26f6ee..b2da275bf 100644
--- a/lib/imdd.h
+++ b/lib/imdd.h
@@ -394,8 +394,87 @@ class imdd_manager {
         imdd* m_dd;
         interval_dd(unsigned lo, unsigned hi, imdd* d): interval(lo, hi), m_dd(d) {}
     };
-    typedef obj_map<imdd, svector<interval> > filter_id_map;
-    typedef obj_map<imdd, svector<interval_dd> > filter_idd_map;
+    template<typename I>
+    class id_map {
+        unsigned m_T;
+        unsigned_vector m_Ts;
+        svector<svector<I>*> m_vecs;
+        unsigned_vector m_alloc;
+        unsigned        m_first_free;
+        void hard_reset() {
+            std::for_each(m_vecs.begin(), m_vecs.end(), delete_proc<svector<I> >());
+            m_alloc.reset();
+            m_first_free = 0;
+            m_vecs.reset();
+            m_Ts.reset();
+            m_T = 0;
+        }
+
+        void allocate_entry(unsigned id) {
+            if (m_vecs[id]) {
+               return;
+            }
+            while (m_first_free < m_alloc.size()) {
+                if (m_vecs[m_first_free] && m_Ts[m_first_free] < m_T) {
+                    svector<I>* v = m_vecs[m_first_free];
+                    m_vecs[m_first_free] = 0;
+                    m_vecs[id] = v;
+                    ++m_first_free;
+                    return;
+                }
+                ++m_first_free;
+            }
+            m_vecs[id] = alloc(svector<I>);
+            m_alloc.push_back(id);
+        }
+    public:
+        id_map():m_T(0) {}
+        ~id_map() { hard_reset(); }
+        void reset() { ++m_T; m_first_free = 0; if (m_T == UINT_MAX) hard_reset(); }
+        svector<I>& init(imdd* d) {
+            unsigned id = d->get_id();
+            if (id >= m_vecs.size()) {
+                m_vecs.resize(id+1);
+                m_Ts.resize(id+1);
+            }
+            if (m_Ts[id] < m_T) {
+                allocate_entry(id);
+                m_vecs[id]->reset();
+                m_Ts[id] = m_T;
+            }
+            return *m_vecs[id];
+        }
+
+        typedef svector<I> data;
+        struct iterator { 
+            unsigned m_offset; 
+            id_map const& m; 
+            iterator(unsigned o, id_map const& m):m_offset(o),m(m) {}
+            data const & operator*() const { return *m.m_vecs[m_offset]; }
+            data const * operator->() const { return &(operator*()); }
+            data * operator->() { return &(operator*()); }
+            iterator & operator++() { ++m_offset; return move_to_used(); }
+            iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
+            bool operator==(iterator const & it) const { return m_offset == it.m_offset; }
+            bool operator!=(iterator const & it) const { return m_offset != it.m_offset; }
+            iterator & move_to_used() {
+                while (m_offset < m.m_vecs.size() &&
+                       m.m_Ts[m_offset] < m.m_T) {
+                    ++m_offset;
+                }
+                return *this;
+            }
+        };         
+        iterator begin() const { return iterator(0, *this).move_to_used(); }
+        iterator end() const { return iterator(m_vecs.size(), *this); }        
+    };
+    typedef id_map<interval >    filter_id_map;
+    typedef id_map<interval_dd > filter_idd_map;
+    filter_id_map        m_nodes;
+    filter_idd_map       m_nodes_dd;
+    svector<interval_dd> m_i_nodes_dd, m_i_nodes_dd_tmp;
+    svector<interval>    m_i_nodes,    m_i_nodes_tmp;
+    unsigned_vector      m_offsets;
     void filter_identical_main3(imdd * d, imdd_ref& r, unsigned num_vars, unsigned * vars, bool destructive, bool memoize_res);
     void filter_identical_main3(imdd * d, imdd_ref& r, unsigned v1, bool del1, unsigned v2, bool del2, bool memoize_res);
     imdd* filter_identical_loop3(imdd * d, unsigned v1, bool del1, unsigned v2, bool del2, bool memoize_res);
diff --git a/lib/rewriter_def.h b/lib/rewriter_def.h
index 0bdb08c13..258a40a58 100644
--- a/lib/rewriter_def.h
+++ b/lib/rewriter_def.h
@@ -37,9 +37,9 @@ void rewriter_tpl<Config>::process_var(var * v) {
         unsigned idx = v->get_idx();
         if (idx < m_bindings.size()) {
             expr * r = m_bindings[m_bindings.size() - idx - 1];
-            TRACE("process_var", tout << "idx: " << idx << " --> " << mk_ismt2_pp(r, m()) << "\n";
+            TRACE("process_var", if (r) tout << "idx: " << idx << " --> " << mk_ismt2_pp(r, m()) << "\n";
                   tout << "bindings:\n";
-                  for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
+                  for (unsigned i = 0; i < m_bindings.size(); i++) if (m_bindings[i]) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
             if (r != 0) {
                 if (m_num_qvars == 0 || is_ground(r)) {
                     result_stack().push_back(r);
diff --git a/shell/datalog_frontend.cpp b/shell/datalog_frontend.cpp
index 83ad81b0a..216203914 100644
--- a/shell/datalog_frontend.cpp
+++ b/shell/datalog_frontend.cpp
@@ -43,11 +43,13 @@ static datalog::execution_context * g_ectx;
 static front_end_params * g_params;
 
 datalog_params::datalog_params():
-    m_default_table("sparse")
+    m_default_table("sparse"),
+    m_default_table_checked(false)
 {}
 
 void datalog_params::register_params(ini_params& p) {
     p.register_symbol_param("DEFAULT_TABLE", m_default_table, "Datalog engine: default table (sparse)");
+    p.register_bool_param("DEFAULT_TABLE_CHECKED", m_default_table_checked, "Wrap default table with a sanity checker");
 }
 
 static void display_statistics(
@@ -129,6 +131,7 @@ unsigned read_datalog(char const * file, datalog_params const& dl_params, front_
     params_ref params;
     params.set_sym(":engine", symbol("datalog"));
     params.set_sym(":default-table", dl_params.m_default_table);
+    params.set_bool(":default-table-checked", dl_params.m_default_table_checked);
 
     datalog::context ctx(m, front_end_params, params);
     size_t watermark = front_end_params.m_memory_high_watermark;
diff --git a/shell/datalog_frontend.h b/shell/datalog_frontend.h
index 52a9273d5..898a7fd97 100644
--- a/shell/datalog_frontend.h
+++ b/shell/datalog_frontend.h
@@ -21,6 +21,7 @@ Revision History:
 
 struct datalog_params {
     symbol m_default_table;
+    bool   m_default_table_checked;
     datalog_params();
     virtual void register_params(ini_params& p);        
 };
diff --git a/test/imdd.cpp b/test/imdd.cpp
index 74f2f4746..f59f87b4f 100644
--- a/test/imdd.cpp
+++ b/test/imdd.cpp
@@ -551,11 +551,37 @@ static void tst21() {
     std::cout << mk_ll_pp(d2, m) << "\n";       
 }
 
+static void tst22() {
+    std::cout << "--------------------------------\n";
+    std::cout << "swap\n";
+    imdd_manager m;
+    imdd_ref d2(m), d3(m), d4(m);
+
+    d2 = m.mk_empty(3);
+    random_gen rand;
+    for (unsigned i = 0; i < 130; ++i) {
+        unsigned a = rand(20);
+        unsigned b = rand(20);
+        unsigned c = rand(20);
+        add_triple(m, d2, a, a, b, b, c, c);
+    }
+    std::cout << mk_ll_pp(d2, m) << "\n";
+
+    m.mk_swap(d2, d3, 0, true);
+    std::cout << mk_ll_pp(d3, m) << "\n";
+
+    m.mk_swap(d3, d4, 0, true);
+    std::cout << mk_ll_pp(d4, m) << "\n";
+    SASSERT(m.is_subset(d2, d4));
+    SASSERT(m.is_subset(d4, d2));
+}
+
 void tst_imdd() {
     // enable_trace("imdd_add_bug");
     // enable_trace("add_facts_bug");
     enable_trace("mk_distinct_imdd");
     enable_trace("mk_union_core");
+    tst22();
     tst0();
     tst1();
     tst2();
@@ -578,5 +604,6 @@ void tst_imdd() {
     tst18();
     tst20();
     tst21();
+
 }