diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 388fd56f3..f8186e446 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -85,6 +85,7 @@ namespace sat {
         }
         
         m_burst_search    = p.burst_search();
+        m_enable_pre_simplify  = p.enable_pre_simplify();
         
         m_max_conflicts   = p.max_conflicts();
         m_num_threads     = p.threads();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index c57aeeffe..5079a61a1 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -108,6 +108,7 @@ namespace sat {
         double             m_random_freq;
         unsigned           m_random_seed;
         unsigned           m_burst_search;
+        bool               m_enable_pre_simplify;
         unsigned           m_max_conflicts;
         unsigned           m_num_threads;
         bool               m_ddfw_search;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 36646006d..74e5f77b4 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -27,6 +27,7 @@ def_module_params('sat',
                           ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
                           ('random_seed', UINT, 0, 'random seed'),
                           ('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
+                          ('enable_pre_simplify', BOOL, False, 'enable pre simplifications before the bounded search'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'),
                           ('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'),
                           ('gc.initial', UINT, 20000, 'learned clauses garbage collection frequency'),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 678858fdd..2a28f5233 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1222,6 +1222,16 @@ namespace sat {
                 do_gc();
             }
 
+            if (m_config.m_enable_pre_simplify) {
+                do_simplify();
+                if (check_inconsistent()) return l_false;
+            }
+
+            if (m_config.m_max_conflicts == 0) {
+                IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
+                return l_undef;
+            }
+
             if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
                 m_restart_threshold = m_config.m_burst_search;
                 lbool r = bounded_search();
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 9b6d062d2..dc90317be 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -229,6 +229,7 @@ tactic * mk_sat_tactic(ast_manager & m, params_ref const & p) {
 tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) {
     params_ref p_aux;
     p_aux.set_uint("max_conflicts", 0);
+    p_aux.set_bool("enable_pre_simplify", true);
     tactic * t = clean(using_params(mk_sat_tactic(m, p), p_aux));
     t->updt_params(p);
     return t;