diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 24d2bca9b..ed951fd93 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -38,8 +38,6 @@ namespace sat {
         m_glue_psm("glue_psm"),
         m_psm_glue("psm_glue") {
         m_num_threads = 1;
-        m_local_search = 0;
-        m_lookahead_search = false;
         m_lookahead_simplify = false;
         m_lookahead_simplify_bca = false;
         m_elim_vars = false;
@@ -92,7 +90,6 @@ namespace sat {
         m_local_search_threads = p.local_search_threads();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();
-        m_lookahead_search = p.lookahead_search();
         if (p.lookahead_reward() == symbol("heule_schur")) {
             m_lookahead_reward = heule_schur_reward;
         }
@@ -195,7 +192,6 @@ namespace sat {
         else {
             throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
         }
-        m_dimacs_inprocess_display  = p.dimacs_inprocess_display();
 
         sat_simplifier_params sp(_p);
         m_elim_vars = sp.elim_vars();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 9a20bbc63..c3018ef29 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -82,7 +82,6 @@ namespace sat {
         unsigned           m_num_threads;
         unsigned           m_local_search_threads;
         bool               m_local_search;
-        bool               m_lookahead_search;
         bool               m_lookahead_simplify;
         bool               m_lookahead_simplify_bca;
         unsigned           m_lookahead_cube_cutoff;
@@ -112,8 +111,6 @@ namespace sat {
         bool               m_drat_check_unsat;
         bool               m_drat_check_sat;
 
-        bool               m_dimacs_inprocess_display;
-
         symbol             m_always_true;
         symbol             m_always_false;
         symbol             m_caching;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 4f65b100b..e8ae53dca 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -35,15 +35,13 @@ def_module_params('sat',
                           ('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'),
                           ('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'),
+                          ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
                           ('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
-                          ('lookahead_search', BOOL, False, 'use lookahead solver'),
                           ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
                           ('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),
                           ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
-                          ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
-                          ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))
+                          ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index f8425b9bc..b3fc95f47 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -950,12 +950,6 @@ namespace sat {
                 if (m_config.m_inprocess_max <= m_simplifications) {
                     m_reason_unknown = "sat.max.inprocess";
                     IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-inprocess\")\n";);
-                    if (m_config.m_dimacs_inprocess_display) {
-                        display_dimacs(std::cout);
-                        for (unsigned i = 0; i < num_lits; ++lits) {
-                            std::cout << dimacs_lit(lits[i]) << " 0\n";
-                        }
-                    }
                     return l_undef;
                 }