diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index d803617f5..ada6f910b 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -32,6 +32,7 @@ def_module_params('sat',
                           ('cardinality.solver', BOOL, False, 'use cardinality solver'),
                           ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'),
                           ('xor.solver', BOOL, False, 'use xor solver'),
+                          ('disable_incremental', BOOL, False, 'disable incremental solving. Allows stronger simplification, but solver cannot be re-used.'),
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index a5f66dfd9..9042587b7 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1044,6 +1044,7 @@ namespace sat {
             clause_use_list::iterator it = occs.mk_iterator();
             while (!it.at_end()) {
                 clause & c = it.curr();
+                it.next();
                 if (c.is_blocked()) continue;
                 m_counter -= c.size();
                 SASSERT(c.contains(l));
@@ -1053,7 +1054,6 @@ namespace sat {
                     s.m_num_blocked_clauses++;
                 }
                 s.unmark_all(c);
-                it.next();
             }
             for (clause* c : m_to_remove) 
                 s.block_clause(*c);
@@ -1086,6 +1086,7 @@ namespace sat {
             while (!it.at_end()) {
                 bool tautology = false;
                 clause & c = it.curr();
+                it.next();
                 if (c.is_blocked()) continue;
                 for (literal lit : c) {
                     if (s.is_marked(~lit) && lit != ~l) {
@@ -1110,7 +1111,6 @@ namespace sat {
                         if (j == 0) return false;
                     }
                 }
-                it.next();
             }
             return first;
         }
@@ -1360,6 +1360,7 @@ namespace sat {
             clause_use_list::iterator it = neg_occs.mk_iterator();
             while (!it.at_end()) {
                 clause & c = it.curr();
+                it.next();
                 if (c.is_blocked()) continue;
                 m_counter -= c.size();
                 unsigned sz = c.size();
@@ -1370,7 +1371,6 @@ namespace sat {
                 }
                 if (i == sz)
                     return false;
-                it.next();
             }
 
             if (s.s.m_ext) {
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 53383a7c2..099dc701b 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -29,6 +29,7 @@ Notes:
 #include "tactic/bv/bit_blaster_tactic.h"
 #include "tactic/core/simplify_tactic.h"
 #include "sat/tactic/goal2sat.h"
+#include "sat/tactic/sat_tactic.h"
 #include "ast/ast_pp.h"
 #include "model/model_smt2_pp.h"
 #include "tactic/filter_model_converter.h"
@@ -848,8 +849,13 @@ private:
 };
 
 
-solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p) {
-    return alloc(inc_sat_solver, m, p);
+solver* mk_inc_sat_solver(ast_manager& m, params_ref const& _p) {
+    sat_params p(_p);
+    if (p.disable_incremental()) {
+        tactic_ref t = mk_sat_tactic(m, _p);
+        return mk_tactic2solver(m, t.get(), _p);
+    }
+    return alloc(inc_sat_solver, m, _p);
 }