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_compiler.cpp b/src/muz_qe/dl_compiler.cpp
index 34dd94214..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;
diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h
index e5b62f54b..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;
 
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 8ac32f4a7..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));
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.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 2da0463e8..96bc8c326 100644
--- a/src/muz_qe/dl_util.h
+++ b/src/muz_qe/dl_util.h
@@ -587,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); }
@@ -765,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 ef5639279..be6d999b6 100644
--- a/src/muz_qe/rel_context.cpp
+++ b/src/muz_qe/rel_context.cpp
@@ -113,10 +113,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/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_ */