diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp
index 37dce5937..7f96d4753 100644
--- a/src/sat/sat_cut_simplifier.cpp
+++ b/src/sat/sat_cut_simplifier.cpp
@@ -576,7 +576,7 @@ namespace sat {
         cuts2bins(cuts);
         bins2dont_cares();
         dont_cares2cuts(cuts);        
-        m_aig_cuts.simplify();
+        // m_aig_cuts.simplify();
     }
 
     /**
@@ -698,16 +698,16 @@ namespace sat {
     }
 
     void cut_simplifier::collect_statistics(statistics& st) const {
-        st.update("sat-aig.eqs",   m_stats.m_num_eqs);
-        st.update("sat-aig.cuts",  m_stats.m_num_cuts);
-        st.update("sat-aig.ands",  m_stats.m_num_ands);
-        st.update("sat-aig.ites",  m_stats.m_num_ites);
-        st.update("sat-aig.xors",  m_stats.m_num_xors);
-        st.update("sat-aig.xands", m_stats.m_xands);
-        st.update("sat-aig.xites", m_stats.m_xites);
-        st.update("sat-aig.xxors", m_stats.m_xxors);
-        st.update("sat-aig.xluts", m_stats.m_xluts);
-        st.update("sat-aig.dc-reduce", m_stats.m_num_dont_care_reductions);
+        st.update("sat-cut.eqs",   m_stats.m_num_eqs);
+        st.update("sat-cut.cuts",  m_stats.m_num_cuts);
+        st.update("sat-cut.ands",  m_stats.m_num_ands);
+        st.update("sat-cut.ites",  m_stats.m_num_ites);
+        st.update("sat-cut.xors",  m_stats.m_num_xors);
+        st.update("sat-cut.xands", m_stats.m_xands);
+        st.update("sat-cut.xites", m_stats.m_xites);
+        st.update("sat-cut.xxors", m_stats.m_xxors);
+        st.update("sat-cut.xluts", m_stats.m_xluts);
+        st.update("sat-cut.dc-reduce", m_stats.m_num_dont_care_reductions);
     }
 
     void cut_simplifier::validate_unit(literal lit) {
diff --git a/src/sat/sat_cut_simplifier.h b/src/sat/sat_cut_simplifier.h
index e59af5ee8..144051ffd 100644
--- a/src/sat/sat_cut_simplifier.h
+++ b/src/sat/sat_cut_simplifier.h
@@ -92,7 +92,7 @@ namespace sat {
 
             struct hash {
                 unsigned operator()(bin_rel const& p) const { 
-                    return mk_mix(p.u, p.v, 1); 
+                    return p.u + 65599*p.v; // Weinberger's should be a bit cheaper mk_mix(p.u, p.v, 1); 
                 }
             };
             struct eq {
diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp
index 9ff37012c..d78c8131e 100644
--- a/src/sat/sat_cutset.cpp
+++ b/src/sat/sat_cutset.cpp
@@ -79,6 +79,9 @@ namespace sat {
 
     void cut_set::push_back(on_update_t& on_add, cut const& c) {
         SASSERT(m_max_size > 0);
+        if (!m_cuts) {
+            m_cuts = new (*m_region) cut[m_max_size];
+        }
         if (m_size == m_max_size) {
             m_max_size *= 2;
             cut* new_cuts = new (*m_region) cut[m_max_size]; 
@@ -109,9 +112,9 @@ namespace sat {
         SASSERT(!m_region || m_cuts);
         VERIFY(!m_region || m_max_size > 0);
         if (!m_region) {
-            m_max_size = max_sz;
+            m_max_size = 2; // max_sz;
             m_region = &r;
-            m_cuts = new (r) cut[max_sz];
+            m_cuts = nullptr;
         }
     }