diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp
index de1d91f3c..55060f2ea 100644
--- a/src/sat/sat_aig_cuts.cpp
+++ b/src/sat/sat_aig_cuts.cpp
@@ -86,7 +86,7 @@ namespace sat {
             return true;
         }
         m_num_cuts++;
-        if (++m_insertions > m_config.m_max_insertions) {
+        if (++m_insertions > max_cutset_size(v)) {
             return false;
         }
         while (cs.size() >= max_cutset_size(v)) {
@@ -412,7 +412,7 @@ namespace sat {
         return result;
     }
 
-    uint64_t aig_cuts::eval(node const& n, svector<uint64_t> const& env) const {
+    cut_val aig_cuts::eval(node const& n, cut_eval const& env) const {
         uint64_t result;
         switch (n.op()) {
         case var_op:
@@ -422,7 +422,7 @@ namespace sat {
             result = ~0ull;
             for (unsigned i = 0; i < n.size(); ++i) {
                 literal u = m_literals[n.offset() + i];
-                uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()];
+                uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
                 result &= uv;
             }
             break;
@@ -430,7 +430,7 @@ namespace sat {
             result = 0ull;
             for (unsigned i = 0; i < n.size(); ++i) {
                 literal u = m_literals[n.offset() + i];
-                uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()];
+                uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
                 result ^= uv;
             }
             break;
@@ -438,9 +438,9 @@ namespace sat {
             literal u = m_literals[n.offset() + 0]; 
             literal v = m_literals[n.offset() + 1]; 
             literal w = m_literals[n.offset() + 2]; 
-            uint64_t uv = u.sign() ? ~env[u.var()] : env[u.var()];
-            uint64_t vv = v.sign() ? ~env[v.var()] : env[v.var()];
-            uint64_t wv = w.sign() ? ~env[w.var()] : env[w.var()];
+            uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
+            uint64_t vv = v.sign() ? env[v.var()].m_f : env[v.var()].m_t;
+            uint64_t wv = w.sign() ? env[w.var()].m_f : env[w.var()].m_t;
             result = (uv & vv) | ((~uv) & wv);
             break;
         }
@@ -448,14 +448,16 @@ namespace sat {
             UNREACHABLE();
         }
         if (n.sign()) result = ~result;
-        return result;
+        return cut_val(result, ~result);
     }
     
-    svector<uint64_t> aig_cuts::simulate(unsigned num_rounds) {
-        svector<uint64_t> result;
+    cut_eval aig_cuts::simulate(unsigned num_rounds) {
+        cut_eval result;
         for (unsigned i = 0; i < m_cuts.size(); ++i) {
-            result.push_back((uint64_t)m_rand() + ((uint64_t)m_rand() << 16ull) + 
-                             ((uint64_t)m_rand() << 32ull) + ((uint64_t)m_rand() << 48ull));
+            uint64_t r = 
+                (uint64_t)m_rand() + ((uint64_t)m_rand() << 16ull) + 
+                ((uint64_t)m_rand() << 32ull) + ((uint64_t)m_rand() << 48ull);
+            result.push_back(cut_val(r, ~r));
         }
         for (unsigned i = 0; i < num_rounds; ++i) {
             for (unsigned j = 0; j < m_cuts.size(); ++j) {
diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h
index 11d413498..2c6f28bb6 100644
--- a/src/sat/sat_aig_cuts.h
+++ b/src/sat/sat_aig_cuts.h
@@ -114,8 +114,6 @@ namespace sat {
         bool insert_aux(unsigned v, node const& n);
         void init_cut_set(unsigned id);
 
-        unsigned max_cutset_size(unsigned v) const { return v == UINT_MAX ? m_config.m_max_cutset_size : m_max_cutset_size[v]; }
-
         bool eq(node const& a, node const& b);
 
         unsigned_vector filter_valid_nodes() const;
@@ -133,7 +131,7 @@ namespace sat {
         void flush_roots(literal_vector const& to_root, node& n);
         void flush_roots(literal_vector const& to_root, cut_set& cs);
 
-        uint64_t eval(node const& n, svector<uint64_t> const& env) const;
+        cut_val eval(node const& n, cut_eval const& env) const;
 
         std::ostream& display(std::ostream& out, node const& n) const;
 
@@ -166,6 +164,7 @@ namespace sat {
         void set_on_clause_del(on_clause_t& on_clause_del);
 
         void inc_max_cutset_size(unsigned v) { m_max_cutset_size[v] += 10; touch(v); }
+        unsigned max_cutset_size(unsigned v) const { return v == UINT_MAX ? m_config.m_max_cutset_size : m_max_cutset_size[v]; }
 
         vector<cut_set> const & operator()();
         unsigned num_cuts() const { return m_num_cuts; }
@@ -174,7 +173,7 @@ namespace sat {
 
         void touch(bool_var v) { m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
 
-        svector<uint64_t> simulate(unsigned num_rounds);
+        cut_eval simulate(unsigned num_rounds);
 
         std::ostream& display(std::ostream& out) const;
 
diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp
index 6027e2f8f..ba5b74b15 100644
--- a/src/sat/sat_aig_simplifier.cpp
+++ b/src/sat/sat_aig_simplifier.cpp
@@ -165,7 +165,7 @@ namespace sat {
             aig2clauses();
             ++i;
         }
-        while (i < m_stats.m_num_calls && n < m_stats.m_num_eqs + m_stats.m_num_units);
+        while (i*i < m_stats.m_num_calls && n < m_stats.m_num_eqs + m_stats.m_num_units);
     }
 
     /**
@@ -425,17 +425,25 @@ namespace sat {
 
         // Assign higher cutset budgets to equality candidates that come from simulation
         // touch them to trigger recomputation of cutsets.
-        u64_map<unsigned> val2var;
+        u64_map<literal> val2lit;
         unsigned i = 0, j = 0, num_eqs = 0;
-        for (uint64_t val : var2val) {
+        for (cut_val val : var2val) {
             if (!s.was_eliminated(i) && s.value(i) == l_undef) {
-                if (val2var.find(val, j)) {
+                literal u(i, false), v;
+                if (val2lit.find(val.m_t, v)) {
+                    
                     m_aig_cuts.inc_max_cutset_size(i);
-                    m_aig_cuts.inc_max_cutset_size(j);
+                    m_aig_cuts.inc_max_cutset_size(v.var());
+                    num_eqs++;
+                }
+                else if (val2lit.find(val.m_f, v)) {
+                    m_aig_cuts.inc_max_cutset_size(i);
+                    m_aig_cuts.inc_max_cutset_size(v.var());
                     num_eqs++;
                 }
                 else {
-                    val2var.insert(val, i);
+                    val2lit.insert(val.m_t, u);
+                    val2lit.insert(val.m_f, ~u);
                 }
             }
             ++i;
diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp
index 460eb4411..1acc34739 100644
--- a/src/sat/sat_cutset.cpp
+++ b/src/sat/sat_cutset.cpp
@@ -166,9 +166,10 @@ namespace sat {
        sat-sweep evaluation. Given 64 bits worth of possible values per variable, 
        find possible values for function table encoded by cut.
     */
-    uint64_t cut::eval(svector<uint64_t> const& env) const {
-        uint64_t result = 0ull;
+    cut_val cut::eval(cut_eval const& env) const {
+        cut_val v;
         uint64_t t = table();
+        uint64_t n = table();
         unsigned sz = size();
         if (sz == 1 && t == 2) {
             return env[m_elems[0]];
@@ -176,11 +177,12 @@ namespace sat {
         for (unsigned i = 0; i < 64; ++i) {
             unsigned offset = 0;
             for (unsigned j = 0; j < sz; ++j) {
-                offset |= (((env[m_elems[j]] >> i) & 0x1) << j);
+                offset |= (((env[m_elems[j]].m_t >> i) & 0x1) << j);
             }
-            result |= ((t >> offset) & 0x1) << i;
+            v.m_t |= ((t >> offset) & 0x1) << i;
+            v.m_f |= ((n >> offset) & 0x1) << i;
         }
-        return result;
+        return v;
     }
     
     std::ostream& cut::display(std::ostream& out) const {
diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h
index eb138e170..af7f4e15d 100644
--- a/src/sat/sat_cutset.h
+++ b/src/sat/sat_cutset.h
@@ -22,6 +22,14 @@
 
 namespace sat {
 
+    struct cut_val {
+        cut_val():m_t(0ull), m_f(0ull) {}
+        cut_val(uint64_t t, uint64_t f): m_t(t), m_f(f) {}
+        uint64_t m_t, m_f;
+    };
+    
+    typedef svector<cut_val> cut_eval;
+
     class cut {
         unsigned m_filter;
         unsigned m_size;
@@ -51,7 +59,7 @@ namespace sat {
             return *this;
         }
 
-        uint64_t eval(svector<uint64_t> const& env) const;
+        cut_val eval(cut_eval const& env) const;
 
         unsigned size() const { return m_size; }