diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index ada6f910b..d803617f5 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -32,7 +32,6 @@ 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_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 099dc701b..15c1cb240 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -850,11 +850,6 @@ private:
 
 
 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);
 }