diff --git a/src/muz_qe/dl_base.h b/src/muz_qe/dl_base.h
index e7243cb70..491bb261d 100644
--- a/src/muz_qe/dl_base.h
+++ b/src/muz_qe/dl_base.h
@@ -656,6 +656,7 @@ namespace datalog {
 
     typedef sort * relation_sort;
     typedef ptr_vector<sort> relation_signature_base0;
+    typedef ptr_hash<sort> relation_sort_hash;
 
     typedef app * relation_element;
     typedef app_ref relation_element_ref;
@@ -739,8 +740,8 @@ namespace datalog {
 
         struct hash {
             unsigned operator()(relation_signature const& s) const { 
-                relation_sort const* sorts = s.c_ptr();
-                return string_hash(reinterpret_cast<char const*>(sorts), sizeof(*sorts)*s.size(), 12); }
+                return obj_vector_hash<relation_signature>(s);
+            }
         };
 
         struct eq {
@@ -816,9 +817,11 @@ namespace datalog {
 
     typedef uint64 table_sort;
     typedef svector<table_sort> table_signature_base0;
+    typedef uint64_hash table_sort_hash;
 
     typedef uint64 table_element;
     typedef svector<table_element> table_fact;
+    typedef uint64_hash table_element_hash;
 
     struct table_traits {
         typedef table_plugin plugin;
@@ -881,8 +884,8 @@ namespace datalog {
     public:
         struct hash {
             unsigned operator()(table_signature const& s) const { 
-                table_sort const* sorts = s.c_ptr();
-                return string_hash(reinterpret_cast<char const*>(sorts), sizeof(*sorts)*s.size(), 12); }
+                return svector_hash<table_sort_hash>()(s);
+            }
         };
 
         struct eq {
diff --git a/src/muz_qe/dl_check_table.h b/src/muz_qe/dl_check_table.h
index 7126bde66..40a3d5207 100644
--- a/src/muz_qe/dl_check_table.h
+++ b/src/muz_qe/dl_check_table.h
@@ -89,15 +89,6 @@ namespace datalog {
 
     class check_table : public table_base {
         friend class check_table_plugin;
-        friend class check_table_plugin::join_fn;
-        friend class check_table_plugin::union_fn;
-        friend class check_table_plugin::transformer_fn;
-        friend class check_table_plugin::rename_fn;
-        friend class check_table_plugin::project_fn;
-        friend class check_table_plugin::filter_equal_fn;
-        friend class check_table_plugin::filter_identical_fn;
-        friend class check_table_plugin::filter_interpreted_fn;
-        friend class check_table_plugin::filter_by_negation_fn;
 
         table_base* m_checker;
         table_base* m_tocheck;
diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp
index 80b9dee5a..e4528426a 100644
--- a/src/muz_qe/dl_compiler.cpp
+++ b/src/muz_qe/dl_compiler.cpp
@@ -36,7 +36,7 @@ namespace datalog {
     }
 
     void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) {
-        pred2idx::entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX);
+        pred2idx::obj_map_entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX);
         if(e->get_data().m_value!=UINT_MAX) {
             //predicate is already loaded
             return;
@@ -421,6 +421,7 @@ namespace datalog {
     void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, 
             reg_idx delta_reg, bool use_widening, instruction_block & acc) {
         
+        ast_manager & m = m_context.get_manager();
         m_instruction_observer.start_rule(r);
 
         const app * h = r->get_head();
@@ -433,7 +434,7 @@ namespace datalog {
         SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin
 
         reg_idx single_res;
-        ptr_vector<expr> single_res_expr;
+        expr_ref_vector single_res_expr(m);
 
         //used to save on filter_identical instructions where the check is already done 
         //by the join operation
@@ -536,7 +537,7 @@ namespace datalog {
             unsigned srlen=single_res_expr.size();
             SASSERT((single_res==execution_context::void_register) ? (srlen==0) : (srlen==m_reg_signatures[single_res].size()));
             for(unsigned i=0; i<srlen; i++) {
-                expr * exp = single_res_expr[i];
+                expr * exp = single_res_expr[i].get();
                 if(is_app(exp)) {
                     SASSERT(m_context.get_decl_util().is_numeral_ext(exp));
                     relation_element value = to_app(exp);
@@ -618,14 +619,13 @@ namespace datalog {
             dealloc = true;
         }
 
-        //enforce interpreted tail predicates
+        // enforce interpreted tail predicates
         unsigned ft_len=r->get_tail_size(); //full tail
         for(unsigned tail_index=ut_len; tail_index<ft_len; tail_index++) {
             app * t = r->get_tail(tail_index);
-            var_idx_set t_vars;
-            ast_manager & m = m_context.get_manager();
-            collect_vars(m, t, t_vars);
-
+            ptr_vector<sort> t_vars;
+            ::get_free_vars(t, t_vars);
+            
             if(t_vars.empty()) {
                 expr_ref simplified(m);
                 m_context.get_rewriter()(t, simplified);
@@ -639,40 +639,23 @@ namespace datalog {
             }
 
             //determine binding size
-            unsigned max_var=0;
-            var_idx_set::iterator vit = t_vars.begin();
-            var_idx_set::iterator vend = t_vars.end();
-            for(; vit!=vend; ++vit) {
-                unsigned v = *vit;
-                if(v>max_var) { max_var = v; }
+            while (!t_vars.back()) {
+                t_vars.pop_back();
             }
+            unsigned max_var = t_vars.size();
 
             //create binding
             expr_ref_vector binding(m);
             binding.resize(max_var+1);
-            vit = t_vars.begin();
-            for(; vit!=vend; ++vit) {
-                unsigned v = *vit;
+            
+            for(unsigned v = 0; v < t_vars.size(); ++v) {
+                if (!t_vars[v]) {
+                    continue;
+                }
                 int2ints::entry * e = var_indexes.find_core(v);
                 if(!e) {
                     //we have an unbound variable, so we add an unbound column for it
-                    relation_sort unbound_sort = 0;
-
-                    for(unsigned hindex = 0; hindex<head_len; hindex++) {
-                        expr * harg = h->get_arg(hindex);
-                        if(!is_var(harg) || to_var(harg)->get_idx()!=v) {
-                            continue;
-                        }
-                        unbound_sort = to_var(harg)->get_sort();
-                    }
-                    if(!unbound_sort) {
-                        // the variable in the interpreted tail is neither bound in the 
-                        // uninterpreted tail nor present in the head
-                        std::stringstream sstm;
-                        sstm << "rule with unbound variable #" << v << " in interpreted tail: ";                       
-                        r->display(m_context, sstm);
-                        throw default_exception(sstm.str());
-                    }
+                    relation_sort unbound_sort = t_vars[v];
 
                     reg_idx new_reg;
                     TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";);
@@ -759,7 +742,7 @@ namespace datalog {
         m_instruction_observer.finish_rule();
     }
 
-    void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, ptr_vector<expr>& single_res_expr, 
+    void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, 
                                                     bool & dealloc, instruction_block & acc) {
         uint_set pos_vars;
         u_map<expr*> neg_vars;
@@ -782,7 +765,7 @@ namespace datalog {
         }
         // populate positive variables:
         for (unsigned i = 0; i < single_res_expr.size(); ++i) {
-            expr* e = single_res_expr[i];
+            expr* e = single_res_expr[i].get();
             if (is_var(e)) {
                 pos_vars.insert(to_var(e)->get_idx());
             }
diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h
index 1dfb7c7d8..8f40f814a 100644
--- a/src/muz_qe/dl_compiler.h
+++ b/src/muz_qe/dl_compiler.h
@@ -41,7 +41,8 @@ namespace datalog {
         typedef hashtable<unsigned, u_hash, u_eq> int_set;
         typedef u_map<unsigned> int2int;
         typedef u_map<unsigned_vector> int2ints;
-        typedef map<func_decl *, reg_idx, ptr_hash<func_decl>,ptr_eq<func_decl> > pred2idx;
+        typedef obj_map<func_decl, reg_idx> pred2idx;
+//        typedef map<func_decl *, reg_idx, ptr_hash<func_decl>,ptr_eq<func_decl> > pred2idx;
         typedef unsigned_vector var_vector;
         typedef ptr_vector<func_decl> func_decl_vector;
 
@@ -177,7 +178,7 @@ namespace datalog {
         void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, 
             instruction_block & acc);
 
-        void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, ptr_vector<expr>& single_res_expr,
+        void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr,
                                               bool & dealloc, instruction_block& acc);
         
         void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, instruction_block & acc);
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index df293aeba..50915946a 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -813,9 +813,7 @@ namespace datalog {
 
     void context::transform_rules() {
         m_transf.reset();
-        if (get_params().filter_rules()) {
-            m_transf.register_plugin(alloc(mk_filter_rules, *this));
-        }
+        m_transf.register_plugin(alloc(mk_filter_rules, *this));        
         m_transf.register_plugin(alloc(mk_simple_joins, *this));
         if (unbound_compressor()) {
             m_transf.register_plugin(alloc(mk_unbound_compressor, *this));
@@ -823,7 +821,14 @@ namespace datalog {
         if (similarity_compressor()) {
             m_transf.register_plugin(alloc(mk_similarity_compressor, *this)); 
         }
-        m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this));
+        m_transf.register_plugin(alloc(mk_partial_equivalence_transformer, *this));
+        m_transf.register_plugin(alloc(mk_rule_inliner, *this));
+        m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this));
+
+        if (get_params().bit_blast()) {
+            m_transf.register_plugin(alloc(mk_bit_blast, *this, 22000));
+            m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this, 21000));
+        }
 
         transform_rules(m_transf);
     }
diff --git a/src/muz_qe/dl_finite_product_relation.h b/src/muz_qe/dl_finite_product_relation.h
index 165422661..d5181d122 100644
--- a/src/muz_qe/dl_finite_product_relation.h
+++ b/src/muz_qe/dl_finite_product_relation.h
@@ -47,7 +47,7 @@ namespace datalog {
             }
             struct hash {
                 unsigned operator()(const rel_spec & o) const {
-                    return o.m_inner_kind^int_vector_hash(o.m_table_cols);
+                    return o.m_inner_kind^svector_hash<bool_hash>()(o.m_table_cols);
                 }
             };
         };
diff --git a/src/muz_qe/dl_mk_filter_rules.h b/src/muz_qe/dl_mk_filter_rules.h
index 4a247fdb5..91751f9b8 100644
--- a/src/muz_qe/dl_mk_filter_rules.h
+++ b/src/muz_qe/dl_mk_filter_rules.h
@@ -45,14 +45,18 @@ namespace datalog {
             filter_key(ast_manager & m) : new_pred(m), filter_args(m) {}
 
             unsigned hash() const {
-                return new_pred->hash() ^ int_vector_hash(filter_args);
+                unsigned r = new_pred->hash();
+                for (unsigned i = 0; i < filter_args.size(); ++i) {
+                    r ^= filter_args[i]->hash();
+                }
+                return r;
             }
             bool operator==(const filter_key & o) const {
                 return o.new_pred==new_pred && vectors_equal(o.filter_args, filter_args);
             }
         };
 
-        typedef map<filter_key*, func_decl*, obj_ptr_hash<filter_key>, deref_eq<filter_key> > filter_cache;
+        typedef obj_map<filter_key, func_decl*> filter_cache;
 
         context &                                 m_context;
         ast_manager &                             m_manager;
diff --git a/src/muz_qe/dl_mk_magic_sets.h b/src/muz_qe/dl_mk_magic_sets.h
index 507f6c2bf..dfc66e7ea 100644
--- a/src/muz_qe/dl_mk_magic_sets.h
+++ b/src/muz_qe/dl_mk_magic_sets.h
@@ -47,6 +47,11 @@ namespace datalog {
             AD_BOUND
         };
 
+        struct a_flag_hash {
+            typedef a_flag data;
+            unsigned operator()(a_flag x) const { return x; }
+        };
+
         struct adornment : public svector<a_flag> {
 
             void populate(app * lit, const var_idx_set & bound_vars);
@@ -71,7 +76,7 @@ namespace datalog {
                 return m_pred==o.m_pred && m_adornment==o.m_adornment;
             }
             unsigned hash() const {
-                return m_pred->hash()^int_vector_hash(m_adornment);
+                return m_pred->hash()^svector_hash<a_flag_hash>()(m_adornment);
             }
         };
 
diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp
index 8e77785b8..b600811f0 100644
--- a/src/muz_qe/dl_mk_similarity_compressor.cpp
+++ b/src/muz_qe/dl_mk_similarity_compressor.cpp
@@ -29,6 +29,7 @@ namespace datalog {
         m_manager(ctx.get_manager()),
         m_threshold_count(ctx.similarity_compressor_threshold()),
         m_result_rules(ctx.get_rule_manager()),
+        m_modified(false),
         m_pinned(m_manager) {
         SASSERT(m_threshold_count>1);
     }
@@ -55,6 +56,9 @@ namespace datalog {
         return (a>b) ? 1 : ( (a==b) ? 0 : -1);
     }
 
+    template<typename T>
+    static int aux_compare(T* a, T* b);
+
     static int compare_var_args(app* t1, app* t2) {
         SASSERT(t1->get_num_args()==t2->get_num_args());
         int res;
@@ -88,7 +92,7 @@ namespace datalog {
             if ((skip_countdown--) == 0) {
                 continue;
             }
-            res = aux_compare(t1->get_arg(i), t2->get_arg(i));
+            res = aux_compare(t1->get_arg(i)->get_id(), t2->get_arg(i)->get_id());
             if (res!=0) { return res; }
         }
         return 0;
@@ -113,7 +117,7 @@ namespace datalog {
         for (int i=-1; i<pos_tail_sz; i++) {
             app * t1 = get_by_tail_index(r1, i);
             app * t2 = get_by_tail_index(r2, i);
-            res = aux_compare(t1->get_decl(), t2->get_decl());
+            res = aux_compare(t1->get_decl()->get_id(), t2->get_decl()->get_id());
             if (res!=0) { return res; }
             res = compare_var_args(t1, t2);
             if (res!=0) { return res; }
@@ -121,7 +125,7 @@ namespace datalog {
 
         unsigned tail_sz = r1->get_tail_size();
         for (unsigned i=pos_tail_sz; i<tail_sz; i++) {
-            res = aux_compare(r1->get_tail(i), r2->get_tail(i));
+            res = aux_compare(r1->get_tail(i)->get_id(), r2->get_tail(i)->get_id());
             if (res!=0) { return res; }
         }
         
diff --git a/src/muz_qe/dl_product_relation.h b/src/muz_qe/dl_product_relation.h
index c5e755939..91c2286a7 100644
--- a/src/muz_qe/dl_product_relation.h
+++ b/src/muz_qe/dl_product_relation.h
@@ -40,8 +40,12 @@ namespace datalog {
         class filter_equal_fn;
         class filter_identical_fn;
         class filter_interpreted_fn;
+        struct fid_hash {
+            typedef family_id data;
+            unsigned operator()(data x) const { return static_cast<unsigned>(x); }
+        };
 
-        rel_spec_store<rel_spec> m_spec_store;
+        rel_spec_store<rel_spec, svector_hash<fid_hash> > m_spec_store;
 
         family_id get_relation_kind(const product_relation & r);
 
diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp
index ef8e6ddd4..986a1f2c4 100644
--- a/src/muz_qe/dl_relation_manager.cpp
+++ b/src/muz_qe/dl_relation_manager.cpp
@@ -740,7 +740,6 @@ namespace datalog {
     relation_transformer_fn * relation_manager::mk_select_equal_and_project_fn(const relation_base & t, 
             const relation_element & value, unsigned col) { 
         relation_transformer_fn * res = t.get_plugin().mk_select_equal_and_project_fn(t, value, col);
-        TRACE("dl", tout << t.get_plugin().get_name() << " " << value << " " << col << "\n";);
         if(!res) {
             relation_mutator_fn * selector = mk_filter_equal_fn(t, value, col);
             if(selector) {
diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h
index 26008a830..f22ae7923 100644
--- a/src/muz_qe/dl_relation_manager.h
+++ b/src/muz_qe/dl_relation_manager.h
@@ -605,7 +605,7 @@ namespace datalog {
     /**
        This is a helper class for relation_plugins whose relations can be of various kinds.
     */
-    template<class Spec, class Hash=int_vector_hash_proc<Spec>, class Eq=vector_eq_proc<Spec> >
+    template<class Spec, class Hash, class Eq=vector_eq_proc<Spec> >
     class rel_spec_store {
         typedef relation_signature::hash r_hash;
         typedef relation_signature::eq r_eq;
diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp
index 0cad08cb4..21021ca43 100644
--- a/src/muz_qe/dl_rule_transformer.cpp
+++ b/src/muz_qe/dl_rule_transformer.cpp
@@ -107,6 +107,9 @@ namespace datalog {
                 tout << typeid(p).name()<<":\n";
                 new_rules->display(tout);
             );
+            IF_VERBOSE(1, new_rules->get_rule(0)->display(m_context, verbose_stream() << typeid(p).name() <<"\n"););
+            IF_VERBOSE(1, verbose_stream() << new_rules->get_dependencies().begin()->m_key->get_name() << "\n";);
+
         }
         if (modified) {
             rules.replace_rules(*new_rules);
diff --git a/src/muz_qe/dl_sieve_relation.h b/src/muz_qe/dl_sieve_relation.h
index d6df3af55..551f5d705 100644
--- a/src/muz_qe/dl_sieve_relation.h
+++ b/src/muz_qe/dl_sieve_relation.h
@@ -52,7 +52,7 @@ namespace datalog {
 
             struct hash {
                 unsigned operator()(const rel_spec & s) const {
-                    return int_vector_hash(s.m_inner_cols)^s.m_inner_kind;
+                    return svector_hash<bool_hash>()(s.m_inner_cols)^s.m_inner_kind;
                 }
             };
         };
diff --git a/src/muz_qe/dl_sparse_table.h b/src/muz_qe/dl_sparse_table.h
index 3920836e6..010277b6b 100644
--- a/src/muz_qe/dl_sparse_table.h
+++ b/src/muz_qe/dl_sparse_table.h
@@ -359,7 +359,7 @@ namespace datalog {
 
         typedef svector<unsigned> key_spec;        //sequence of columns in a key
         typedef svector<table_element> key_value;  //values of key columns
-        typedef map<key_spec, key_indexer*, int_vector_hash_proc<key_spec>,
+        typedef map<key_spec, key_indexer*, svector_hash_proc<unsigned_hash>,
             vector_eq_proc<key_spec> > key_index_map;
 
         static const store_offset NO_RESERVE = UINT_MAX;
diff --git a/src/muz_qe/dl_table.h b/src/muz_qe/dl_table.h
index 8dc0a355b..3a240c337 100644
--- a/src/muz_qe/dl_table.h
+++ b/src/muz_qe/dl_table.h
@@ -73,7 +73,7 @@ namespace datalog {
 
         class our_iterator_core;
 
-        typedef hashtable<table_fact, int_vector_hash_proc<table_fact>, 
+        typedef hashtable<table_fact, svector_hash_proc<table_element_hash>, 
             vector_eq_proc<table_fact> > storage;
 
         storage m_data;
diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h
index 974ab5862..96bc8c326 100644
--- a/src/muz_qe/dl_util.h
+++ b/src/muz_qe/dl_util.h
@@ -207,7 +207,9 @@ namespace datalog {
         static unsigned expr_cont_get_size(app * a) { return a->get_num_args(); }
         static expr * expr_cont_get(app * a, unsigned i) { return a->get_arg(i); }
         static unsigned expr_cont_get_size(const ptr_vector<expr> & v) { return v.size(); }
+        static unsigned expr_cont_get_size(const expr_ref_vector & v) { return v.size(); }
         static expr * expr_cont_get(const ptr_vector<expr> & v, unsigned i) { return v[i]; }
+        static expr * expr_cont_get(const expr_ref_vector & v, unsigned i) { return v[i]; }
     public:
         variable_intersection(ast_manager & m) : m_consts(m) {}
 
@@ -585,17 +587,31 @@ namespace datalog {
     }
 
     template<class T>
-    unsigned int_vector_hash(const T & cont) {
-        return string_hash(reinterpret_cast<const char *>(cont.c_ptr()), 
-            cont.size()*sizeof(typename T::data), 0);
+    struct default_obj_chash {
+        unsigned operator()(T const& cont, unsigned i) const {
+            return cont[i]->hash();
+        }
+    };
+    template<class T>
+    unsigned obj_vector_hash(const T & cont) {
+        return get_composite_hash(cont, cont.size(),default_kind_hash_proc<T>(), default_obj_chash<T>());
     }
 
     template<class T>
-    struct int_vector_hash_proc { 
+    struct obj_vector_hash_proc { 
         unsigned operator()(const T & cont) const {
-            return int_vector_hash(cont);
+            return obj_vector_hash(cont);
         } 
     };
+
+    template<class T>
+    struct svector_hash_proc { 
+        unsigned operator()(const svector<typename T::data> & cont) const {
+            return svector_hash<T>()(cont);
+        } 
+    };
+
+
     template<class T>
     struct vector_eq_proc { 
         bool operator()(const T & c1, const T & c2) const { return vectors_equal(c1, c2); }
@@ -763,11 +779,6 @@ namespace datalog {
     //
     // -----------------------------------
 
-    struct uint64_hash {
-        typedef uint64 data;
-        unsigned operator()(uint64 x) const { return hash_ull(x); }
-    };
-
     template<class T>
     void universal_delete(T* ptr) {
         dealloc(ptr);
diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp
index 898edf123..07633c536 100644
--- a/src/muz_qe/rel_context.cpp
+++ b/src/muz_qe/rel_context.cpp
@@ -116,10 +116,12 @@ namespace datalog {
         TRACE("dl", m_context.display(tout););
 
         while (true) {
+            
             m_ectx.reset();
             m_code.reset();
             termination_code.reset();
             m_context.ensure_closed();
+            IF_VERBOSE(1, verbose_stream() << "num rules: " << m_context.get_rules().get_num_rules() << "\n";);
             m_context.transform_rules();
             if (m_context.canceled()) {
                 result = l_undef;
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 4140f683c..9c80d8c34 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -259,8 +259,6 @@ namespace smt {
         theory_var                     m_zero_int; // cache the variable representing the zero variable.
         theory_var                     m_zero_real; // cache the variable representing the zero variable.
         int_vector                     m_scc_id;                  // Cheap equality propagation
-        bool                           m_modified_since_eq_prop;  // true if new constraints were asserted 
-                                                                  // since last eq propagation.
         eq_prop_info_set               m_eq_prop_info_set;        // set of existing equality prop infos
         ptr_vector<eq_prop_info>       m_eq_prop_infos;
 
@@ -289,18 +287,14 @@ namespace smt {
         virtual theory_var mk_var(enode* n);
 
         virtual theory_var mk_var(app* n);
-                
-        void mark_as_modified_since_eq_prop();
-        
-        void unmark_as_modified_since_eq_prop();
-        
-        bool propagate_cheap_equalities();
-
+                        
         void compute_delta();
 
         void found_non_diff_logic_expr(expr * n);
 
-        bool is_interpreted(app* n) const;
+        bool is_interpreted(app* n) const {
+            return get_family_id() == n->get_family_id();
+        }
 
         void del_clause_eh(clause* cls);
 
@@ -312,7 +306,6 @@ namespace smt {
             m_arith_eq_adapter(*this, params, m_util),
             m_zero_int(null_theory_var),
             m_zero_real(null_theory_var),
-            m_modified_since_eq_prop(false),
             m_asserted_qhead(0),
             m_num_core_conflicts(0),
             m_num_propagation_calls(0),
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 7493f81c2..6700b4c37 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -374,8 +374,12 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
     // either will already be zero (as we don't do mixed constraints).
     m_graph.set_to_zero(m_zero_int, m_zero_real);
     SASSERT(is_consistent());
+<<<<<<< HEAD
 
     
+=======
+   
+>>>>>>> d849dbf21f218663e9c9ffa01eea168c7b7765c9
     if (m_non_diff_logic_exprs) {
         return FC_GIVEUP; 
     }
@@ -533,22 +537,6 @@ bool theory_diff_logic<Ext>::propagate_atom(atom* a) {
     return true;
 }
 
-
-
-template<typename Ext>
-void theory_diff_logic<Ext>::mark_as_modified_since_eq_prop() {
-    if (!m_modified_since_eq_prop) {
-        get_context().push_trail(value_trail<context, bool>(m_modified_since_eq_prop));
-        m_modified_since_eq_prop = true;
-    }
-}
-
-template<typename Ext>
-void theory_diff_logic<Ext>::unmark_as_modified_since_eq_prop() {
-    get_context().push_trail(value_trail<context, bool>(m_modified_since_eq_prop));
-    m_modified_since_eq_prop = false;
-}
-
 template<typename Ext>
 void theory_diff_logic<Ext>::del_clause_eh(clause* cls) {
     
@@ -795,7 +783,6 @@ theory_var theory_diff_logic<Ext>::mk_num(app* n, rational const& r) {
 
 template<typename Ext>
 theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
-    mark_as_modified_since_eq_prop();
     theory_var v = theory::mk_var(n);
     TRACE("diff_logic_vars", tout << "mk_var: " << v << "\n";);
     m_graph.init_var(v);
@@ -803,10 +790,6 @@ theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
     return v;
 }
 
-template<typename Ext>
-bool theory_diff_logic<Ext>::is_interpreted(app* n) const {
-    return n->get_family_id() == get_family_id();
-}
 
 template<typename Ext>
 theory_var theory_diff_logic<Ext>::mk_var(app* n) {
@@ -847,7 +830,6 @@ void theory_diff_logic<Ext>::reset_eh() {
     m_asserted_atoms   .reset();
     m_stats            .reset();
     m_scopes           .reset();
-    m_modified_since_eq_prop = false;
     m_asserted_qhead        = 0;
     m_num_core_conflicts    = 0;
     m_num_propagation_calls = 0;
@@ -858,70 +840,6 @@ void theory_diff_logic<Ext>::reset_eh() {
 }
 
 
-template<typename Ext>
-bool theory_diff_logic<Ext>::propagate_cheap_equalities() {
-    bool result = false;
-    TRACE("dl_new_eq", get_context().display(tout););
-    context& ctx = get_context();
-    region&  reg = ctx.get_region();
-    SASSERT(m_eq_prop_info_set.empty());
-    SASSERT(m_eq_prop_infos.empty());
-    if (m_modified_since_eq_prop) {
-        m_graph.compute_zero_edge_scc(m_scc_id);
-        int n = get_num_vars();
-        for (theory_var v = 0; v < n; v++) {
-            rational delta_r;
-            theory_var x_v = expand(true, v, delta_r);
-            numeral delta(delta_r);
-            int scc_id = m_scc_id[x_v];
-            if (scc_id != -1) {
-                delta += m_graph.get_assignment(x_v);
-                TRACE("eq_scc", tout << v << " " << x_v << " " << scc_id << " " << delta << "\n";);
-                eq_prop_info info(scc_id, delta);
-                typename eq_prop_info_set::entry * entry = m_eq_prop_info_set.find_core(&info);
-                if (entry == 0) {
-                    eq_prop_info * new_info = alloc(eq_prop_info, scc_id, delta, v);
-                    m_eq_prop_info_set.insert(new_info);
-                    m_eq_prop_infos.push_back(new_info);
-                }
-                else {
-                    // new equality found
-                    theory_var r = entry->get_data()->get_root();
-                    
-                    enode * n1 = get_enode(v);
-                    enode * n2 = get_enode(r);
-                    if (n1->get_root() != n2->get_root()) {
-                        // r may be an alias (i.e., it is not realy in the graph). So, I should expand it. 
-                        // nsb: ?? 
-                        rational r_delta;
-                        theory_var x_r = expand(true, r, r_delta);
-                        
-                        justification* j = new (reg) implied_eq_justification(*this, x_v, x_r, m_graph.get_timestamp());
-                        (void)j;
-
-                        m_stats.m_num_th2core_eqs++;
-                        // TBD: get equality into core.
-
-                        NOT_IMPLEMENTED_YET();
-                        // new_eq_eh(x_v, x_r, *j);
-                        result = true;
-                    }
-                }
-            }
-        }
-        m_eq_prop_info_set.reset();
-        std::for_each(m_eq_prop_infos.begin(), m_eq_prop_infos.end(), delete_proc<eq_prop_info>());
-        m_eq_prop_infos.reset();
-        unmark_as_modified_since_eq_prop();        
-    }
-
-    TRACE("dl_new_eq", get_context().display(tout););
-    SASSERT(!m_modified_since_eq_prop);
-
-    return result;
-}
-
-
 template<typename Ext>
 void theory_diff_logic<Ext>::compute_delta() {
     m_delta = rational(1);
@@ -1080,7 +998,6 @@ void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v
         // assign the corresponding equality literal.
         //
 
-        mark_as_modified_since_eq_prop();
 
         app_ref eq(m), s2(m), t2(m);
         app* s1 = get_enode(s)->get_owner();
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 831efa087..2c2afab6f 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -371,6 +371,12 @@ struct ctx_simplify_tactic::imp {
         if (!modified) {
             r = t;
         }
+        else if (new_new_args.empty()) {
+            r = OR?m.mk_false():m.mk_true();
+        }
+        else if (new_new_args.size() == 1) {
+            r = new_new_args[0];
+        }
         else {
             std::reverse(new_new_args.c_ptr(), new_new_args.c_ptr() + new_new_args.size());
             m_mk_app(t->get_decl(), new_new_args.size(), new_new_args.c_ptr(), r);
diff --git a/src/util/hash.h b/src/util/hash.h
index 3c7e50a6c..4232dd2af 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -20,6 +20,7 @@ Revision History:
 #define _HASH_H_
 
 #include<algorithm>
+#include"util.h"
 
 #ifndef __fallthrough
 #define __fallthrough
@@ -142,6 +143,11 @@ struct size_t_hash {
     unsigned operator()(size_t x) const { return static_cast<unsigned>(x); }
 };
 
+struct uint64_hash {
+    typedef uint64 data;
+    unsigned operator()(uint64 x) const { return static_cast<unsigned>(x); }
+};
+
 struct bool_hash {
     typedef bool data;
     unsigned operator()(bool x) const { return static_cast<unsigned>(x); }
diff --git a/src/util/vector.h b/src/util/vector.h
index 704452d0f..c9ed900a9 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -432,24 +432,29 @@ typedef svector<unsigned> unsigned_vector;
 typedef svector<char> char_vector;
 typedef svector<double> double_vector;
 
-template<typename Hash>
-struct vector_hash {
+template<typename Hash, typename Vec>
+struct vector_hash_tpl {
     Hash m_hash;
-    typedef vector<typename Hash::data> data;
+    typedef Vec data;
 
     unsigned operator()(data const& v, unsigned idx) const { return m_hash(v[idx]); }
 
-    vector_hash(Hash const& h = Hash()):m_hash(h) {}
+    vector_hash_tpl(Hash const& h = Hash()):m_hash(h) {}
 
     unsigned operator()(data const& v) const {
         if (v.empty()) {
             return 778;
         }
-        return get_composite_hash<data, default_kind_hash_proc<data>, vector_hash>(v, v.size());
+        return get_composite_hash<data, default_kind_hash_proc<data>, vector_hash_tpl>(v, v.size());
     }
-
 };
 
+template<typename Hash>
+struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> > {};
+
+template<typename Hash>
+struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
+
 
 #endif /* _VECTOR_H_ */