diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 3ccd183c2..a5f66dfd9 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -974,9 +974,9 @@ namespace sat {
         void operator()() {
             if (s.bce_enabled())
                 block_clauses();
-            if (s.m_cce) 
+            if (s.cce_enabled()) 
                 cce();
-            if (s.m_bca)
+            if (s.bca_enabled())
                 bca();
     }
 
@@ -1176,7 +1176,7 @@ namespace sat {
                     is_tautology = add_cla(blocked);
                 }
                 while (m_covered_clause.size() > sz && !is_tautology);
-                if (s.m_acce && !is_tautology) {
+                if (s.acce_enabled() && !is_tautology) {
                     sz = m_covered_clause.size();
                     add_ala();
                 }
@@ -1338,11 +1338,9 @@ namespace sat {
                 }                
                 if (!found) {
                     IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
-                    watched w(l2, false);
-                    w.set_blocked();
+                    watched w(l2, true);
                     s.get_wlist(~l).push_back(w);
-                    w = watched(l, false);
-                    w.set_blocked();
+                    w = watched(l, true);
                     s.get_wlist(~l2).push_back(w);
                     ++s.m_num_bca;
                 }
diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg
index 6528e6699..07088a60b 100644
--- a/src/sat/sat_simplifier_params.pyg
+++ b/src/sat/sat_simplifier_params.pyg
@@ -20,6 +20,6 @@ def_module_params(module_name='sat',
                           ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
                           ('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'),
                           ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
-	                  ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
+                          ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
                           ('subsumption', BOOL, True, 'eliminate subsumed clauses'),
                           ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))