diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp
index e6be3da98..a57e5d194 100644
--- a/src/ast/ast_translation.cpp
+++ b/src/ast/ast_translation.cpp
@@ -23,6 +23,7 @@ Revision History:
 #include "ast/format.h"
 #include "ast/ast_translation.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/ast_pp.h"
 
 ast_translation::~ast_translation() {
     reset_cache();
@@ -47,7 +48,12 @@ void ast_translation::reset_cache() {
 void ast_translation::cache(ast * s, ast * t) {
     SASSERT(!m_cache.contains(s));
     if (s->get_ref_count() > 1) {
+        if (m_insert_count > (1 << 17)) {
+            reset_cache();
+            m_insert_count = 0;
+        }
         m_cache.insert(s, t);
+        ++m_insert_count;
         m_from_manager.inc_ref(s);
         m_to_manager.inc_ref(t);
     }
@@ -76,9 +82,15 @@ void ast_translation::push_frame(ast * n) {
 
 bool ast_translation::visit(ast * n) {        
     ast * r;
-    if (n->get_ref_count() > 1 && m_cache.find(n, r)) {
-        m_result_stack.push_back(r);
-        return true;
+    if (n->get_ref_count() > 1) {
+        if (m_cache.find(n, r)) {
+            m_result_stack.push_back(r);
+            ++m_hit_count;
+            return true;
+        }
+        else {
+            ++m_miss_count;
+        }
     }
     push_frame(n);
     return false;
@@ -187,20 +199,32 @@ ast * ast_translation::process(ast const * _n) {
     SASSERT(m_frame_stack.empty());
     SASSERT(m_extra_children_stack.empty());
     
+    ++m_num_process;
+    if (m_num_process > (1 << 16)) {
+        reset_cache();
+        m_num_process = 0;
+    }
     if (!visit(const_cast<ast*>(_n))) {
         while (!m_frame_stack.empty()) {
         loop:
+            ++m_loop_count;
             frame & fr = m_frame_stack.back();
             ast * n = fr.m_n;
             ast * r;         
             TRACE("ast_translation", tout << mk_ll_pp(n, m_from_manager, false) << "\n";);
-            if (fr.m_idx == 0 && n->get_ref_count() > 1 && m_cache.find(n, r)) {
-                SASSERT(m_result_stack.size() == fr.m_rpos);
-                m_result_stack.push_back(r);
-                m_extra_children_stack.shrink(fr.m_cpos);
-                m_frame_stack.pop_back();
-                TRACE("ast_translation", tout << "hit\n";);
-                continue;
+            if (fr.m_idx == 0 && n->get_ref_count() > 1) {
+                if (m_cache.find(n, r)) {
+                    SASSERT(m_result_stack.size() == fr.m_rpos);
+                    m_result_stack.push_back(r);
+                    m_extra_children_stack.shrink(fr.m_cpos);
+                    m_frame_stack.pop_back();
+                    TRACE("ast_translation", tout << "hit\n";);
+                    m_hit_count++;
+                    continue;
+                }
+                else {
+                    m_miss_count++;
+                }
             }
             switch (n->get_kind()) {
             case AST_VAR: {
diff --git a/src/ast/ast_translation.h b/src/ast/ast_translation.h
index 9d09fbb76..47517a073 100644
--- a/src/ast/ast_translation.h
+++ b/src/ast/ast_translation.h
@@ -37,6 +37,11 @@ class ast_translation {
     ptr_vector<ast>     m_extra_children_stack; // for sort and func_decl, since they have nested AST in their parameters
     ptr_vector<ast>     m_result_stack; 
     obj_map<ast, ast*>  m_cache;
+    unsigned            m_loop_count;
+    unsigned            m_hit_count;
+    unsigned            m_miss_count;
+    unsigned            m_insert_count;
+    unsigned            m_num_process;
 
     void cache(ast * s, ast * t);
     void collect_decl_extra_children(decl * d);
@@ -50,6 +55,11 @@ class ast_translation {
 
 public:
     ast_translation(ast_manager & from, ast_manager & to, bool copy_plugins = true) : m_from_manager(from), m_to_manager(to) {
+        m_loop_count = 0;
+        m_hit_count = 0;
+        m_miss_count = 0;
+        m_insert_count = 0;
+        m_num_process = 0;
         if (&from != &to) {
             if (copy_plugins)
                 m_to_manager.copy_families_plugins(m_from_manager);
@@ -73,6 +83,12 @@ public:
 
     void reset_cache();
     void cleanup();
+    
+    unsigned loop_count() const { return m_loop_count; }
+    unsigned hit_count() const { return m_hit_count; }
+    unsigned miss_count() const { return m_miss_count; }
+    unsigned insert_count() const { return m_insert_count; }
+    unsigned long long get_num_collision() const { return m_cache.get_num_collision(); }
 };
 
 // Translation with non-persistent cache.
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 09610a3a7..73bb94c7d 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -87,24 +87,18 @@ namespace sat {
         else  
             throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'");
 
-        if (p.lookahead_cube_cutoff() == symbol("depth")) {
+        if (p.lookahead_cube_cutoff() == symbol("depth")) 
             m_lookahead_cube_cutoff = depth_cutoff;
-        }
-        else if (p.lookahead_cube_cutoff() == symbol("freevars")) {
+        else if (p.lookahead_cube_cutoff() == symbol("freevars")) 
             m_lookahead_cube_cutoff = freevars_cutoff;
-        }
-        else if (p.lookahead_cube_cutoff() == symbol("psat")) {
+        else if (p.lookahead_cube_cutoff() == symbol("psat")) 
             m_lookahead_cube_cutoff = psat_cutoff;
-        }
-        else if (p.lookahead_cube_cutoff() == symbol("adaptive_freevars")) {
+        else if (p.lookahead_cube_cutoff() == symbol("adaptive_freevars")) 
             m_lookahead_cube_cutoff = adaptive_freevars_cutoff;
-        }
-        else if (p.lookahead_cube_cutoff() == symbol("adaptive_psat")) {
+        else if (p.lookahead_cube_cutoff() == symbol("adaptive_psat")) 
             m_lookahead_cube_cutoff = adaptive_psat_cutoff;
-        }
-        else {
+        else 
             throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'depth', 'freevars', 'psat', 'adaptive_freevars' and 'adaptive_psat'");
-        }
         m_lookahead_cube_fraction = p.lookahead_cube_fraction();
         m_lookahead_cube_depth = p.lookahead_cube_depth();
         m_lookahead_cube_freevars = p.lookahead_cube_freevars();
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index fa9fef180..e7b57d7f6 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -24,11 +24,12 @@ Revision History:
 #include<limits.h>
 #include "util/memory_manager.h"
 #include "util/hash.h"
+#include "util/vector.h"
 
 #define DEFAULT_HASHTABLE_INITIAL_CAPACITY 8
 #define SMALL_TABLE_CAPACITY               64
 
-// #define HASHTABLE_STATISTICS
+//  #define HASHTABLE_STATISTICS
 
 #ifdef HASHTABLE_STATISTICS
 #define HS_CODE(CODE) { CODE }
@@ -375,8 +376,7 @@ public:
     } ((void) 0)
 
     void insert(data && e) {
-        if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) {
-            // if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
+        if (((m_size + m_num_deleted) << 2) > (m_capacity * 3)) {
             expand_table();
         }
         unsigned hash     = get_hash(e);
@@ -488,7 +488,9 @@ public:
         else if (curr->is_free()) {                                             \
             return 0;                                                           \
         }                                                                       \
-        HS_CODE(const_cast<core_hashtable*>(this)->m_st_collision++;);          \
+        else {                                                                  \
+            HS_CODE(const_cast<core_hashtable*>(this)->m_st_collision++;);      \
+        }                                                                       \
     } ((void) 0)
 
     entry * find_core(data const & e) const {
@@ -655,7 +657,33 @@ public:
     unsigned long long get_num_collision() const { return 0; }
 #endif
 
-    
+#define COLL_LOOP_BODY() {                                              \
+    if (curr->is_used()) {                                          \
+        if (curr->get_hash() == hash && equals(curr->get_data(), e)) return; \
+        collisions.push_back(curr->get_data());                         \
+        continue;                                                       \
+    }                                                                   \
+    else if (curr->is_free()) {                                         \
+        continue;                                                       \
+    }                                                                   \
+    collisions.push_back(curr->get_data());                             \
+    } ((void) 0);    
+
+    void get_collisions(data const& e, vector<data>& collisions) {        
+        unsigned hash = get_hash(e);
+        unsigned mask = m_capacity - 1;
+        unsigned idx  = hash & mask;
+        entry * begin = m_table + idx;
+        entry * end   = m_table + m_capacity;
+        entry * curr  = begin;
+        for (; curr != end; ++curr) {
+            COLL_LOOP_BODY();
+        }
+        for (curr = m_table; curr != begin; ++curr) {
+            COLL_LOOP_BODY();
+        }
+
+    }
 };
 
 template<typename T, typename HashProc, typename EqProc>
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index df279383b..dc876ffb2 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -204,6 +204,14 @@ public:
 
     unsigned long long get_num_collision() const { return m_table.get_num_collision(); }
 
+    void get_collisions(Key * k, vector<Key*>& collisions) {
+        vector<key_data> cs;
+        m_table.get_collisions(key_data(k), cs);
+        for (key_data const& kd : cs) {
+            collisions.push_back(kd.m_key);
+        }
+    }
+
     void swap(obj_map & other) {
         m_table.swap(other.m_table);
     }