diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp
index de050525f..65377caed 100644
--- a/src/sat/sat_bceq.cpp
+++ b/src/sat/sat_bceq.cpp
@@ -428,6 +428,8 @@ namespace sat {
 
 
     void bceq::operator()() {
+        if (!m_solver.m_config.m_bcd) return;
+        flet<bool> _disable_bcd(m_solver.m_config.m_bcd, false);
         use_list     ul;        
         solver       s(m_solver.m_params, 0);
         m_use_list = &ul;
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 17eda1707..d2a662b64 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -107,6 +107,7 @@ namespace sat {
         m_minimize_core   = p.minimize_core();
         m_minimize_core_partial   = p.minimize_core_partial();
         m_optimize_model  = p.optimize_model();
+        m_bcd             = p.bcd();
         m_dyn_sub_res     = p.dyn_sub_res();
     }
 
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 044c91989..021810f3d 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -71,6 +71,7 @@ namespace sat {
         bool               m_minimize_core;
         bool               m_minimize_core_partial;
         bool               m_optimize_model;
+        bool               m_bcd;
 
 
         symbol             m_always_true;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index b0be62eef..1e2551740 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -21,4 +21,5 @@ def_module_params('sat',
                           ('minimize_core', BOOL, False, 'minimize computed core'),
                           ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
+                          ('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))