diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 3f98018c8..f76c3406c 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -127,7 +127,6 @@ namespace polysat {
     *
     * We can assume that op_constraint is only asserted positive.
     */
-
     void op_constraint::narrow(solver& s, bool is_positive) {
         SASSERT(is_positive);
 
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index dd9b526b8..a87ce9f47 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -51,7 +51,7 @@ namespace polysat {
         m_assignment.push_back({p, r});
     }
 
-    void search_state::pop_asssignment() {
+    void search_state::pop_assignment() {
         m_assignment.pop_back();
     }
 
diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index edac55526..bb66bb8f2 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -66,7 +66,7 @@ namespace polysat {
         void push_boolean(sat::literal lit);
         void pop();
 
-        void pop_asssignment();
+        void pop_assignment();
 
         void set_resolved(unsigned i) { m_items[i].set_resolved(); }
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index ad6cc3e67..27f2dc536 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -48,7 +48,6 @@ namespace polysat {
 
     void solver::updt_params(params_ref const& p) {
         m_params.append(p);
-        m_branch_bool = m_params.get_bool("branch_bool", false);
         m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
         m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
     }
@@ -394,10 +393,7 @@ namespace polysat {
     void solver::decide() {
         LOG_H2("Decide");
         SASSERT(can_decide());
-        if (m_branch_bool && m_bvars.can_decide())
-            bdecide(m_bvars.next_var());
-        else
-            pdecide(m_free_pvars.next_var());
+        pdecide(m_free_pvars.next_var());
     }
 
     void solver::pdecide(pvar v) {
@@ -423,10 +419,6 @@ namespace polysat {
         }
     }   
 
-    void solver::bdecide(sat::bool_var b) {
-        decide_bool(sat::literal(b), nullptr);
-    }
-
     void solver::assign_core(pvar v, rational const& val, justification const& j) {
         if (j.is_decision()) 
             ++m_stats.m_num_decisions;
@@ -485,7 +477,7 @@ namespace polysat {
                 // Resolve over variable assignment
                 pvar v = item.var();
                 if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) {
-                    m_search.pop_asssignment();
+                    m_search.pop_assignment();
                     continue;
                 }
                 inc_activity(v);
@@ -494,7 +486,7 @@ namespace polysat {
                     revert_decision(v);
                     return;
                 }
-                m_search.pop_asssignment();
+                m_search.pop_assignment();
             }
             else {
                 // Resolve over boolean literal
@@ -701,13 +693,6 @@ namespace polysat {
             decide_bool(*lemma);
     }
 
-    void solver::decide_bool(sat::literal lit, clause* lemma) {
-        SASSERT(!can_propagate());
-        SASSERT(!is_conflict());
-        push_level();        
-        assign_decision(lit, lemma);
-    }
-
     unsigned solver::level(sat::literal lit0, clause const& cl) {
         unsigned lvl = base_level();
         for (auto lit : cl) {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 1d56e7425..f7113c843 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -94,9 +94,6 @@ namespace polysat {
 
         uint64_t                 m_max_conflicts = std::numeric_limits<uint64_t>::max();
         uint64_t                 m_max_decisions = std::numeric_limits<uint64_t>::max();
-        bool                     m_branch_bool = false;
-
-
 
         // Per constraint state
         constraint_manager       m_constraints;
@@ -177,7 +174,7 @@ namespace polysat {
         void set_conflict(clause& cl) { m_conflict.set(cl); }
         void set_conflict(pvar v) { m_conflict.set(v); }
 
-        bool can_decide() const { return !m_free_pvars.empty() || (m_branch_bool && m_bvars.can_decide()); }
+        bool can_decide() const { return !m_free_pvars.empty(); }
         void decide();
         void pdecide(pvar v);
         void bdecide(sat::bool_var b);