diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 9d3ee864d..69050ed71 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -153,7 +153,6 @@ def_module_params('fixedpoint',
                           ('spacer.eager_reach_check', BOOL, True, 'SPACER: eagerly check if a query is reachable using reachability facts of predecessors'),
                           ('spacer.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'),
                           ('spacer.reset_obligation_queue', BOOL, True, 'SPACER: reset obligation queue when entering a new level'),
-                          ('spacer.init_reach_facts', BOOL, True, 'SPACER: initialize reachability facts with false'),
                           ('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'),
                           ('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),	
                           ('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"), 
@@ -161,7 +160,6 @@ def_module_params('fixedpoint',
                           ('spacer.skip_propagate', BOOL, False, "Skip propagate/pushing phase. Turns PDR into a BMC that returns either reachable or unknown"),
                           ('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"),
                           ('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
-                          ('spacer.reach_as_init', BOOL, True, "Extend initial rules with computed reachability facts"),
                           ('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"),
                           ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"),
                           ('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"),
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index b27bd724e..2349ea03a 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1019,7 +1019,7 @@ void pred_transformer::add_reach_fact (reach_fact *fact)
     expr_ref fml (m);
 
     if (!m_reach_case_vars.empty()) {last_var = m_reach_case_vars.back();}
-    if (fact->is_init () || !ctx.get_params ().spacer_reach_as_init ())
+    if (fact->is_init ())
     {new_var = mk_fresh_reach_case_var();}
     else {
         new_var = extend_initial (fact->get ())->get_arg (0);
@@ -1308,7 +1308,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
                     expr_ref a(m);
                     pm.formula_n2o(pt.get_last_reach_case_var (), a, i);
                     reach_assumps.push_back(m.mk_not (a));
-                } else if (ctx.get_params().spacer_init_reach_facts()) {
+                } else {
                     reach_assumps.push_back(m.mk_not (entry.m_key));
                     break;
                 }