diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index ee4b7c2e4..3e1c6f0cd 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/smt/params/preprocessor_params.cpp
@@ -46,7 +46,6 @@ void preprocessor_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_eliminate_term_ite);
     DISPLAY_PARAM(m_macro_finder);
     DISPLAY_PARAM(m_propagate_values);
-    DISPLAY_PARAM(m_propagate_booleans);
     DISPLAY_PARAM(m_refine_inj_axiom);
     DISPLAY_PARAM(m_eliminate_bounds);
     DISPLAY_PARAM(m_simplify_bit2int);
diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h
index be7fd4c01..f6724fada 100644
--- a/src/smt/params/preprocessor_params.h
+++ b/src/smt/params/preprocessor_params.h
@@ -37,7 +37,6 @@ struct preprocessor_params : public pattern_inference_params,
     bool            m_eliminate_term_ite;
     bool            m_macro_finder;
     bool            m_propagate_values;
-    bool            m_propagate_booleans;
     bool            m_refine_inj_axiom;
     bool            m_eliminate_bounds;
     bool            m_simplify_bit2int;
@@ -59,7 +58,6 @@ public:
         m_eliminate_term_ite(false),
         m_macro_finder(false),
         m_propagate_values(true),
-        m_propagate_booleans(false), // TODO << check peformance
         m_refine_inj_axiom(true),
         m_eliminate_bounds(false),
         m_simplify_bit2int(false),
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 55ea55663..3ab40cdc3 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -574,7 +574,6 @@ namespace smt {
         m_params.m_bv_cc               = false;
         m_params.m_bb_ext_gates        = true;
         m_params.m_nnf_cnf             = false;
-        m_params.m_propagate_booleans  = true;
         m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params));
         setup_arrays();
     }
@@ -644,7 +643,6 @@ namespace smt {
         m_params.m_restart_factor          = 1.5;
         m_params.m_eliminate_bounds        = true;
         m_params.m_qi_quick_checker        = MC_UNSAT;
-        m_params.m_propagate_booleans      = true;
         m_params.m_qi_lazy_threshold       = 20;
         // m_params.m_qi_max_eager_multipatterns = 10; /// <<< HACK
         m_params.m_mbqi                    = true; // enabling MBQI and MACRO_FINDER by default :-)
@@ -672,7 +670,6 @@ namespace smt {
         m_params.m_phase_selection         = PS_ALWAYS_FALSE;
         m_params.m_eliminate_bounds        = true;
         m_params.m_qi_quick_checker        = MC_UNSAT;
-        m_params.m_propagate_booleans      = true;
         m_params.m_qi_eager_threshold      = 5;
         // Added for MBQI release
         m_params.m_qi_lazy_threshold       = 20;