diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp
index f035388e1..607c1213e 100644
--- a/src/sat/sat_aig_cuts.cpp
+++ b/src/sat/sat_aig_cuts.cpp
@@ -24,35 +24,40 @@ namespace sat {
         m_config.m_max_cut_size = std::min(cut().max_cut_size, m_config.m_max_cut_size);
         m_cut_set1.init(m_region, m_config.m_max_cutset_size + 1);
         m_cut_set2.init(m_region, m_config.m_max_cutset_size + 1);
-        m_true = null_bool_var;
+        m_num_cut_calls = 0;
     }
 
-    vector<cut_set> const& aig_cuts::get_cuts() {
+    vector<cut_set> const& aig_cuts::operator()() {
         flush_roots();
         unsigned_vector node_ids = filter_valid_nodes();
         TRACE("aig_simplifier", display(tout););
         augment(node_ids);
         TRACE("aig_simplifier", display(tout););
+        ++m_num_cut_calls;
         return m_cuts;
     }
 
     void aig_cuts::augment(unsigned_vector const& ids) {
         for (unsigned id : ids) {
-            cut_set& cs = m_cuts[id];
-            node const& n = m_aig[id];
-            SASSERT(n.is_valid());
-            // cs.display(std::cout << "augment " << id << "\nbefore\n");
-            augment(n, cs);
-            for (node const& n2 : m_aux_aig[id]) {
-                augment(n2, cs);
+            if (m_aig[id].empty()) {
+                continue;
             }
-            // cs.display(std::cout << "after\n");
+            IF_VERBOSE(3, m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n"));
+            for (node const& n : m_aig[id]) {
+                augment(id, n);
+            }
+            IF_VERBOSE(3, m_cuts[id].display(verbose_stream() << "after\n"));            
         }
     }
 
-    void aig_cuts::augment(node const& n, cut_set& cs) {
-        unsigned nc = n.is_var() ? 0 : n.num_children();
-        if (n.is_var()) {
+    void aig_cuts::augment(unsigned id, node const& n) {
+        unsigned nc = n.size();
+        m_insertions = 0;
+        cut_set& cs = m_cuts[id];
+        if (!is_touched(n)) {
+            // no-op
+        }
+        else if (n.is_var()) {
             SASSERT(!n.sign());
         }
         else if (n.is_ite()) {
@@ -70,23 +75,30 @@ namespace sat {
         else if (nc < m_config.m_max_cut_size) {
             augment_aigN(n, cs);
         }
+        if (m_insertions > 0) {
+            touch(id);
+        }
     }
 
     bool aig_cuts::insert_cut(cut const& c, cut_set& cs) {
-        SASSERT(c.m_size > 0);
+        if (!cs.insert(c)) {
+            return true;
+        }
+        if (++m_insertions > m_config.m_max_insertions) {
+            return false;
+        }
         while (cs.size() >= m_config.m_max_cutset_size) {
             // never evict the first entry, it is used for the starting point
             unsigned idx = 1 + (m_rand() % (cs.size() - 1));
             cs.evict(idx);
         }
-        return cs.insert(c);
+        return true;
     }
 
     void aig_cuts::augment_ite(node const& n, cut_set& cs) {
         literal l1 = child(n, 0);
         literal l2 = child(n, 1);
         literal l3 = child(n, 2);
-        unsigned round = 0;
         for (auto const& a : m_cuts[l1.var()]) {
             for (auto const& b : m_cuts[l2.var()]) {
                 cut ab;
@@ -107,8 +119,7 @@ namespace sat {
                     abc.set_table((t1 & t2) | (~t1 & t3));
                     if (n.sign()) abc.negate();
                     // extract tree size: abc.m_tree_size = a.m_tree_size + b.m_tree_size + c.m_tree_size + 1;
-                    if (insert_cut(abc, cs) && ++round >= m_config.m_max_insertions) 
-                        return;
+                    if (!insert_cut(abc, cs)) return;
                 } 
             }
         }
@@ -116,28 +127,19 @@ namespace sat {
 
     void aig_cuts::augment_aig0(node const& n, cut_set& cs) {
         SASSERT(n.is_and());
-        SASSERT(m_true != null_bool_var);
-        cut c(m_true);          
         cs.reset();
-        if (n.sign()) {
-            c.m_table = 0x0; // constant false
-        }
-        else {
-            c.m_table = 0x3; // constant true
-        }
+        cut c;          
+        c.m_table = (n.sign() ? 0x0 : 0x1);
         cs.push_back(c);
     }
 
     void aig_cuts::augment_aig1(node const& n, cut_set& cs) {
         SASSERT(n.is_and());
         literal lit = child(n, 0);
-        unsigned round = 0;
         for (auto const& a : m_cuts[lit.var()]) {
-            cut c(lit.var());
-            c.set_table(a.m_table);
+            cut c(a);
             if (n.sign()) c.negate();
-            if (insert_cut(c, cs) && ++round >= m_config.m_max_insertions) 
-                return;
+            if (!insert_cut(c, cs)) return; 
         }
     }
 
@@ -145,7 +147,6 @@ namespace sat {
         SASSERT(n.is_and() || n.is_xor());
         literal l1 = child(n, 0);
         literal l2 = child(n, 1);
-        unsigned round = 0;
         for (auto const& a : m_cuts[l1.var()]) {
             for (auto const& b : m_cuts[l2.var()]) {
                 cut c;
@@ -157,8 +158,7 @@ namespace sat {
                     uint64_t t3 = n.is_and() ? t1 & t2 : t1 ^ t2;
                     c.set_table(t3);
                     if (n.sign()) c.negate();
-                    if (insert_cut(c, cs) && ++round >= m_config.m_max_insertions) 
-                        return;
+                    if (!insert_cut(c, cs)) return;
                 }
             }
         }
@@ -174,10 +174,10 @@ namespace sat {
                 m_cut_set1.back().negate();
             }
         }
-        for (unsigned i = 1; i < n.num_children(); ++i) {
+        for (unsigned i = 1; i < n.size(); ++i) {
             m_cut_set2.reset();
             literal lit = child(n, i);
-            unsigned round = 0;
+            m_insertions = 0;
             for (auto const& a : m_cut_set1) {
                 for (auto const& b : m_cuts[lit.var()]) {
                     cut c;
@@ -187,36 +187,45 @@ namespace sat {
                         if (lit.sign()) t2 = ~t2;
                         uint64_t t3 = n.is_and() ? t1 & t2 : t1 ^ t2;
                         c.set_table(t3);
-                        if (i + 1 == n.num_children() && n.sign()) c.negate();
-                        if (insert_cut(c, m_cut_set2) && ++round >= m_config.m_max_insertions) {
-                            break;
-                        }
+                        if (i + 1 == n.size() && n.sign()) c.negate();
+                        if (!insert_cut(c, m_cut_set2)) goto next_child;
                     }
                 }
-                if (round >= m_config.m_max_insertions) {
-                    break;
-                }
             }
+        next_child:
             m_cut_set1.swap(m_cut_set2);
         }
+        m_insertions = 0;
         for (auto & cut : m_cut_set1) {
-            insert_cut(cut, cs);
+            if (!insert_cut(cut, cs)) {
+                break;
+            }
+        }        
+    }
+
+    bool aig_cuts::is_touched(node const& n) {
+        for (unsigned i = 0; i < n.size(); ++i) {
+            literal lit = m_literals[n.offset() + i];
+            if (is_touched(lit)) {
+                return true;
+            }
         }
+        return false;
     }
 
     void aig_cuts::reserve(unsigned v) {
         m_aig.reserve(v + 1);
         m_cuts.reserve(v + 1);
-        m_aux_aig.reserve(v + 1);
+        m_last_touched.reserve(v + 1, 0);
     }
 
     void aig_cuts::add_var(unsigned v) {
         reserve(v);
-        if (!m_aig[v].is_valid()) {
-            m_aig[v] = node(v);
+        if (m_aig[v].empty()) {
+            m_aig[v].push_back(node(v));
             init_cut_set(v);
+            touch(v);
         }
-        SASSERT(m_aig[v].is_valid());
     }
 
     void aig_cuts::add_node(literal head, bool_op op, unsigned sz, literal const* args) {
@@ -230,26 +239,24 @@ namespace sat {
             std::sort(m_literals.c_ptr() + offset, m_literals.c_ptr() + offset + sz);
         }
         for (unsigned i = 0; i < sz; ++i) {
-            if (!m_aig[args[i].var()].is_valid()) {
+            if (m_aig[args[i].var()].empty()) {
                 add_var(args[i].var());
             }
         }
-        if (n.is_const() && m_true == null_bool_var) {
-            m_true = v;
-        }
-        if (!m_aig[v].is_valid() || m_aig[v].is_var() || n.is_const()) {
-            m_aig[v] = n;
+        if (m_aig[v].empty() || n.is_const()) {
+            m_aig[v].reset();
+            m_aig[v].push_back(n);
             init_cut_set(v);
             if (n.is_const()) {
                 augment_aig0(n, m_cuts[v]);
             }
+            touch(v);
         }
-        else if (m_aig[v].is_const() || eq(n, m_aig[v]) || !insert_aux(v, n)) {
+        else if (m_aig[v][0].is_const() || !insert_aux(v, n)) {
             m_literals.shrink(m_literals.size() - sz);
             TRACE("aig_simplifier", tout << "duplicate\n";);
         }
-        for (auto const& c : m_cuts[v]) SASSERT(c.m_size > 0); 
-        SASSERT(m_aig[v].is_valid());
+        SASSERT(!m_aig[v].empty());
     }
 
     void aig_cuts::set_root(bool_var v, literal r) {
@@ -270,17 +277,14 @@ namespace sat {
             to_root[v] = r.sign() ? ~rr : rr;
         }
         for (unsigned i = 0; i < m_aig.size(); ++i) {
-            node& n = m_aig[i];
             // invalidate nodes that have been rooted
             if (to_root[i] != literal(i, false)) {
-                m_aux_aig[i].reset();
-                m_aig[i] = node();
+                m_aig[i].reset();
                 m_cuts[i].reset();
             }
-            else if (n.is_valid()) {
-                flush_roots(to_root, n);
-                for (node & n2 : m_aux_aig[i]) {
-                    flush_roots(to_root, n2);
+            else {
+                for (node & n : m_aig[i]) {
+                    flush_roots(to_root, n);
                 }
             }
         }
@@ -293,10 +297,7 @@ namespace sat {
 
     void aig_cuts::flush_roots(literal_vector const& to_root, node& n) {
         bool changed = false;
-        if (n.is_var()) {
-            return;
-        }
-        for (unsigned i = 0; i < n.num_children(); ++i) {
+        for (unsigned i = 0; i < n.size(); ++i) {
             literal& lit = m_literals[n.offset() + i];
             if (to_root[lit.var()] != lit) {
                 changed = true;
@@ -304,7 +305,7 @@ namespace sat {
             }
         }
         if (changed && (n.is_and() || n.is_xor())) {
-            std::sort(m_literals.c_ptr() + n.offset(), m_literals.c_ptr() + n.offset() + n.num_children());
+            std::sort(m_literals.c_ptr() + n.offset(), m_literals.c_ptr() + n.offset() + n.size());
         }
     }
 
@@ -323,41 +324,71 @@ namespace sat {
     }
 
     void aig_cuts::init_cut_set(unsigned id) {
-        node const& n = m_aig[id];
+        SASSERT(m_aig[id].size() == 1);
+        node const& n = m_aig[id][0];
         SASSERT(n.is_valid());
         auto& cut_set = m_cuts[id];
         cut_set.init(m_region, m_config.m_max_cutset_size + 1);
         cut_set.reset();
         cut_set.push_back(cut(id));  
-        m_aux_aig[id].reset();        
     }
 
     bool aig_cuts::eq(node const& a, node const& b) {
         if (a.is_valid() != b.is_valid()) return false;
         if (!a.is_valid()) return true;
-        if (a.op() != b.op() || a.sign() != b.sign() || a.num_children() != b.num_children()) return false;
-        for (unsigned i = 0; i < a.num_children(); ++i) {
+        if (a.op() != b.op() || a.sign() != b.sign() || a.size() != b.size()) return false;
+        for (unsigned i = 0; i < a.size(); ++i) {
             if (m_literals[a.offset() + i] != m_literals[b.offset() + i]) return false;
         }
         return true;
     }
 
     bool aig_cuts::insert_aux(unsigned v, node const& n) {
-        if (m_aux_aig[v].size() > m_config.m_max_aux) {
-            return false;
-        }
-        for (node const& n2 : m_aux_aig[v]) {
+        unsigned num_gt = 0, num_eq = 0;
+        for (node const& n2 : m_aig[v]) {
             if (eq(n, n2)) return false;
+            else if (n.size() < n2.size()) num_gt++;
+            else if (n.size() == n2.size()) num_eq++;
         }
-        m_aux_aig[v].push_back(n);
-        return true;
+        if (m_aig[v].size() < m_config.m_max_aux) {
+            m_aig[v].push_back(n);
+            touch(v);
+            return true;
+        }
+        if (num_gt > 0) {
+            unsigned idx = rand() % num_gt;
+            for (node const& n2 : m_aig[v]) {
+                if (n.size() < n2.size()) {
+                    if (idx == 0) {
+                        m_aig[v][idx] = n;
+                        touch(v);
+                        return true;
+                    }
+                    --idx;
+                }
+            }
+        }
+        if (num_eq > 0) {
+            unsigned idx = rand() % num_eq;
+            for (node const& n2 : m_aig[v]) {
+                if (n.size() == n2.size()) {
+                    if (idx == 0) {
+                        m_aig[v][idx] = n;
+                        touch(v);
+                        return true;
+                    }
+                    --idx;
+                }
+            }
+        }
+        return false;
     }
 
     unsigned_vector aig_cuts::filter_valid_nodes() const {
         unsigned id = 0;
         unsigned_vector result;
-        for (node const& n : m_aig) {
-            if (n.is_valid()) result.push_back(id);
+        for (auto& v : m_aig) {
+            if (!v.empty()) result.push_back(id);
             ++id;
         }
         return result;
@@ -367,9 +398,10 @@ namespace sat {
         auto ids = filter_valid_nodes();
         for (auto id : ids) {
             out << id << " == ";
-            display(out, m_aig[id]) << "\n";
-            for (auto const& n : m_aux_aig[id]) {
-                display(out << "   ", n) << "\n";
+            bool first = true;
+            for (auto const& n : m_aig[id]) {
+                if (first) first = false; else out << "   ";
+                display(out, n) << "\n";
             }
             m_cuts[id].display(out);
         }
@@ -377,15 +409,15 @@ namespace sat {
     }
 
     std::ostream& aig_cuts::display(std::ostream& out, node const& n) const {
-        if (n.sign()) out << "! ";
+        out << (n.sign() ? "! " : "  ");
         switch (n.op()) {
-        case var_op: out << "var "; return out;
+        case var_op: out << "var "; break;
         case and_op: out << "& "; break;
         case xor_op: out << "^ "; break;
         case ite_op: out << "? "; break;
         default: break;
         }
-        for (unsigned i = 0; i < n.num_children(); ++i) {
+        for (unsigned i = 0; i < n.size(); ++i) {
             out << m_literals[n.offset() + i] << " ";
         }
         return out;
diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h
index 41eb0f436..63f9569f0 100644
--- a/src/sat/sat_aig_cuts.h
+++ b/src/sat/sat_aig_cuts.h
@@ -7,9 +7,20 @@
 
   Abstract:
    
-    extract AIG definitions from clauses
+    Extract AIG definitions from clauses.
     Perform cut-set enumeration to identify equivalences.
 
+    AIG extraction is incremental.
+    It can be called repeatedly.
+    Initially, a main aig node is inserted 
+    (from initial clauses or the input 
+    clausification in goal2sat).
+    Then, auxiliary AIG nodes can be inserted
+    by walking the current set of main and learned 
+    clauses. AIG nodes with fewer arguments are preferred.
+    
+    
+
   Author:
 
     Nikolaj Bjorner 2020-01-02
@@ -48,43 +59,50 @@ namespace sat {
             unsigned m_max_cutset_size;
             unsigned m_max_aux;
             unsigned m_max_insertions;
-            config(): m_max_cut_size(4), m_max_cutset_size(10), m_max_aux(3), m_max_insertions(10) {}
+            config(): m_max_cut_size(4), m_max_cutset_size(10), m_max_aux(5), m_max_insertions(10) {}
         };
 
         // encodes one of var, and, !and, xor, !xor, ite, !ite.
         class node {
             bool     m_sign;
             bool_op  m_op;
-            unsigned m_num_children;
+            unsigned m_size;
             unsigned m_offset;
         public:
-            node(): m_sign(false), m_op(no_op), m_num_children(UINT_MAX), m_offset(UINT_MAX) {}
-            explicit node(unsigned v): m_sign(false), m_op(var_op), m_num_children(UINT_MAX), m_offset(v) {}
-            explicit node(bool negate, bool_op op, unsigned nc, unsigned o): 
-                m_sign(negate), m_op(op), m_num_children(nc), m_offset(o) {}
+            node(): 
+                m_sign(false), m_op(no_op), m_size(UINT_MAX), m_offset(UINT_MAX) {}
+            explicit node(unsigned v) : 
+                m_sign(false), m_op(var_op), m_size(0), m_offset(v) {}
+            explicit node(bool sign, bool_op op, unsigned nc, unsigned o) : 
+                m_sign(sign), m_op(op), m_size(nc), m_offset(o) {}
             bool is_valid() const { return m_offset != UINT_MAX; }
             bool_op op() const { return m_op; }
             bool is_var() const { return m_op == var_op; }
             bool is_and() const { return m_op == and_op; }
             bool is_xor() const { return m_op == xor_op; }
             bool is_ite() const { return m_op == ite_op; }
-            bool is_const() const { return is_and() && num_children() == 0; }
+            bool is_const() const { return is_and() && size() == 0; }
             unsigned var() const { SASSERT(is_var()); return m_offset; }
             bool sign() const { return m_sign; }
-            unsigned num_children() const { SASSERT(!is_var()); return m_num_children; }
+            unsigned size() const { return m_size; }
             unsigned offset() const { return m_offset; }
         };
         random_gen            m_rand;
         config                m_config;
-        svector<node>         m_aig;        // vector of main aig nodes.
-        vector<svector<node>> m_aux_aig;    // vector of auxiliary aig nodes.
+        vector<svector<node>> m_aig;    
         literal_vector        m_literals;
         region                m_region;
         cut_set               m_cut_set1, m_cut_set2;
         vector<cut_set>       m_cuts;
-        bool_var              m_true;
+        unsigned_vector       m_last_touched;
+        unsigned              m_num_cut_calls;
         svector<std::pair<bool_var, literal>> m_roots;
+        unsigned              m_insertions;
 
+        bool is_touched(node const& n);
+        bool is_touched(literal lit) const { return is_touched(lit.var()); }
+        bool is_touched(bool_var v) const { return m_last_touched[v] + m_aig.size() >= m_num_cut_calls * m_aig.size(); }
+        void touch(bool_var v) { m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
         void reserve(unsigned v);
         bool insert_aux(unsigned v, node const& n);
         void init_cut_set(unsigned id);
@@ -93,7 +111,7 @@ namespace sat {
 
         unsigned_vector filter_valid_nodes() const;
         void augment(unsigned_vector const& ids);
-        void augment(node const& n, cut_set& cs);
+        void augment(unsigned id, node const& n);
         void augment_ite(node const& n, cut_set& cs);
         void augment_aig0(node const& n, cut_set& cs);
         void augment_aig1(node const& n, cut_set& cs);
@@ -108,7 +126,7 @@ namespace sat {
 
         std::ostream& display(std::ostream& out, node const& n) const;
 
-        literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.num_children()); return m_literals[n.offset() + idx]; }
+        literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.size()); return m_literals[n.offset() + idx]; }
 
     public:
         aig_cuts();
@@ -116,7 +134,7 @@ namespace sat {
         void add_node(literal head, bool_op op, unsigned sz, literal const* args);
         void set_root(bool_var v, literal r);
 
-        vector<cut_set> const & get_cuts();
+        vector<cut_set> const & operator()();
 
         std::ostream& display(std::ostream& out) const;
     };
diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp
index 6044624f8..f09e500ba 100644
--- a/src/sat/sat_aig_simplifier.cpp
+++ b/src/sat/sat_aig_simplifier.cpp
@@ -26,15 +26,24 @@ namespace sat {
     struct aig_simplifier::report {
         aig_simplifier& s;
         stopwatch       m_watch;
-        report(aig_simplifier& s): s(s) { m_watch.start(); }
+        unsigned        m_num_eqs, m_num_units, m_num_cuts;
+        
+        report(aig_simplifier& s): s(s) { 
+            m_watch.start(); 
+            m_num_eqs   = s.m_stats.m_num_eqs;
+            m_num_units = s.m_stats.m_num_units;
+            m_num_cuts  = s.m_stats.m_num_cuts;
+        }
         ~report() {
+            unsigned ne = s.m_stats.m_num_eqs - m_num_eqs;
+            unsigned nu = s.m_stats.m_num_units - m_num_units;
+            unsigned nc = s.m_stats.m_num_cuts - m_num_cuts;
             IF_VERBOSE(2, 
-                       verbose_stream() << "(sat.aig-simplifier" 
-                       << " :num-eqs " << s.m_stats.m_num_eqs 
-                       << " :num-cuts " << s.m_stats.m_num_cuts 
-                       << " :mb " << mem_stat()
-                       << m_watch 
-                       << ")\n");
+                       verbose_stream() << "(sat.aig-simplifier";
+                       if (ne > 0) verbose_stream() << " :num-eqs "   << ne;
+                       if (nu > 0) verbose_stream() << " :num-units " << nu;
+                       if (nc > 0) verbose_stream() << " :num-cuts "  << nc;
+                       verbose_stream() << " :mb " << mem_stat() << m_watch << ")\n");
         }
     };
 
@@ -83,8 +92,15 @@ namespace sat {
     void aig_simplifier::operator()() {
         report _report(*this);
         TRACE("aig_simplifier", s.display(tout););
-        clauses2aig();
-        aig2clauses();
+        unsigned n = 0, i = 0;
+        ++m_stats.m_num_calls;
+        do {
+            n = m_stats.m_num_eqs + m_stats.m_num_units;
+            clauses2aig();
+            aig2clauses();
+            ++i;
+        }
+        while (i < m_stats.m_num_calls && n < m_stats.m_num_eqs + m_stats.m_num_units);
     }
 
     /**
@@ -114,6 +130,7 @@ namespace sat {
         af.set(on_and);
         af.set(on_ite);
         clause_vector clauses(s.clauses());
+        clauses.append(s.learned());
         af(clauses);
 
         std::function<void (literal_vector const&)> on_xor = 
@@ -147,7 +164,7 @@ namespace sat {
     }
 
     void aig_simplifier::aig2clauses() {
-        vector<cut_set> const& cuts = m_aig_cuts.get_cuts();
+        vector<cut_set> const& cuts = m_aig_cuts();
         map<cut const*, unsigned, cut::hash_proc, cut::eq_proc> cut2id;
         
         union_find_default_ctx ctx;
@@ -160,8 +177,25 @@ namespace sat {
         bool new_eq = false;
         for (unsigned i = cuts.size(); i-- > 0; ) {
             m_stats.m_num_cuts += cuts[i].size();
+
             for (auto& cut : cuts[i]) {
                 unsigned j = 0;
+                if (cut.is_true()) {
+                    if (s.value(i) == l_undef) {
+                        IF_VERBOSE(2, verbose_stream() << "!!!new unit " << literal(i, false) << "\n");
+                        s.assign_unit(literal(i, false));
+                        ++m_stats.m_num_units;
+                    }
+                    break;
+                }
+                if (cut.is_false()) {
+                    if (s.value(i) == l_undef) {
+                        IF_VERBOSE(2, verbose_stream() << "!!!new unit " << literal(i, true) << "\n");
+                        s.assign_unit(literal(i, true));
+                        ++m_stats.m_num_units;
+                    }
+                    break;
+                }
                 if (cut2id.find(&cut, j)) {
                     if (i == j) std::cout << "dup: " << i << "\n";
                     VERIFY(i != j);
diff --git a/src/sat/sat_aig_simplifier.h b/src/sat/sat_aig_simplifier.h
index 5d88033f7..4ffacfedc 100644
--- a/src/sat/sat_aig_simplifier.h
+++ b/src/sat/sat_aig_simplifier.h
@@ -26,7 +26,8 @@ namespace sat {
     class aig_simplifier {
     public:
         struct stats {
-            unsigned m_num_eqs, m_num_cuts, m_num_xors, m_num_ands, m_num_ites;
+            unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_xors, m_num_ands, m_num_ites;
+            unsigned m_num_calls;
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp
index 227638ee0..4863c5b92 100644
--- a/src/sat/sat_cutset.cpp
+++ b/src/sat/sat_cutset.cpp
@@ -70,7 +70,6 @@ namespace sat {
         return out;
     }
 
-    
     /**
        \brief shift table 'a' by adding elements from 'c'.
        a.shift_table(c)
@@ -92,9 +91,7 @@ namespace sat {
        - pre-compute some shift operations.
        - use strides on some common cases.
        - what ABC does?
-    */
-    
-    
+    */       
     uint64_t cut::shift_table(cut const& c) const {
         SASSERT(subset_of(c));
         unsigned index = 0;
diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h
index 2e9288e4c..95cf577fc 100644
--- a/src/sat/sat_cutset.h
+++ b/src/sat/sat_cutset.h
@@ -30,6 +30,10 @@ namespace sat {
 
         cut(unsigned id): m_filter(1u << (id & 0x1F)), m_size(1), m_table(2) { m_elems[0] = id; }
 
+        cut(cut const& other): m_filter(other.m_filter), m_size(other.m_size), m_table(other.m_table) {
+            for (unsigned i = 0; i < m_size; ++i) m_elems[i] = other.m_elems[i];
+        }
+
         unsigned const* begin() const { return m_elems; }
         unsigned const* end() const  { return m_elems + m_size; }
 
@@ -46,7 +50,11 @@ namespace sat {
         }
         void sort();
         void negate() { set_table(~m_table); }
-        void set_table(uint64_t t) { m_table = t & ((1ull << (1ull << m_size)) - 1ull); }
+        uint64_t table_mask() const { return (1ull << (1ull << m_size)) - 1ull; }
+        void set_table(uint64_t t) { m_table = t & table_mask(); }
+
+        bool is_true()  const { return 0 == (table_mask() & ~m_table); }
+        bool is_false() const { return 0 == (table_mask() &  m_table); }
 
         bool operator==(cut const& other) const;
         unsigned hash() const;
@@ -66,7 +74,6 @@ namespace sat {
         uint64_t shift_table(cut const& other) const;
 
         bool merge(cut const& a, cut const& b, unsigned max_sz) {
-            SASSERT(a.m_size > 0 && b.m_size > 0);
             unsigned i = 0, j = 0;
             unsigned x = a[i];
             unsigned y = b[j];