diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 4823b2af1..f5ff21521 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -106,6 +106,7 @@ namespace sat {
         m_anf_exlin         = p.anf_exlin();
         m_cut_simplify      = p.cut();
         m_cut_delay         = p.cut_delay();
+        m_cut_aig           = p.cut_aig();
         m_cut_lut           = p.cut_lut();
         m_cut_xor           = p.cut_xor();
         m_cut_dont_cares    = p.cut_dont_cares();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index e125f89e0..8bc609246 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -123,6 +123,7 @@ namespace sat {
         bool               m_binspr;
         bool               m_cut_simplify;
         unsigned           m_cut_delay;
+        bool               m_cut_aig;
         bool               m_cut_lut;
         bool               m_cut_xor;
         bool               m_cut_dont_cares;
diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp
index 7f96d4753..641a4b703 100644
--- a/src/sat/sat_cut_simplifier.cpp
+++ b/src/sat/sat_cut_simplifier.cpp
@@ -181,6 +181,8 @@ namespace sat {
             literal lit = s.trail_literal(m_trail_size);
             m_aig_cuts.add_node(lit, and_op, 0, 0);
         }
+
+        clause_vector clauses(s.clauses());
                
         std::function<void (literal head, literal_vector const& ands)> on_and = 
             [&,this](literal head, literal_vector const& ands) {
@@ -193,13 +195,13 @@ namespace sat {
             m_aig_cuts.add_node(head, ite_op, 3, args);
             m_stats.m_xites++;
         };
-
-        aig_finder af(s);
-        af.set(on_and);
-        af.set(on_ite);
-        clause_vector clauses(s.clauses());
-        if (m_config.m_learned2aig) clauses.append(s.learned());
-        af(clauses);        
+        if (s.m_config.m_cut_aig) {
+            aig_finder af(s);
+            af.set(on_and);
+            af.set(on_ite);
+            if (m_config.m_learned2aig) clauses.append(s.learned());
+            af(clauses);        
+        }
 
         std::function<void (literal_vector const&)> on_xor = 
             [&,this](literal_vector const& xors) {
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index c0e742966..c32c4335f 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -76,6 +76,7 @@ def_module_params('sat',
                           ('anf.exlin', BOOL, False, 'enable extended linear simplification'), 
 		          ('cut', BOOL, False, 'enable AIG based simplification in-processing'),
 	                  ('cut.delay', UINT, 2, 'delay cut simplification by in-processing round'),
+                          ('cut.aig',   BOOL, False, 'extract aigs (and ites) from cluases for cut simplification'),
                           ('cut.lut',   BOOL, False, 'extract luts from clauses for cut simplification'),
                           ('cut.xor',   BOOL, False, 'extract xors from clauses for cut simplification'),
                           ('cut.dont_cares', BOOL, True, 'integrate dont cares with cuts'),