diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp
index d30da7341..01261a7d3 100644
--- a/src/math/polysat/conflict_core.cpp
+++ b/src/math/polysat/conflict_core.cpp
@@ -212,7 +212,7 @@ namespace polysat {
         if (lemma->size() == 1)
             c->set_unit_clause(lemma.get());
         if (s().m_bvars.value(c.blit()) == l_undef)
-            s().propagate_bool_at(s().level(*lemma), c.blit(), lemma.get());
+            s().assign_bool(s().level(*lemma), c.blit(), lemma.get(), nullptr);
     }
 
     clause_builder conflict_core::build_core_lemma() {
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 3e3ffc715..99810b6d0 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -124,7 +124,7 @@ namespace polysat {
         if (first) 
             s.set_conflict(cl);        
         else 
-            s.propagate_bool_at(s.level(cl), cl[0], &cl);
+            s.assign_bool(s.level(cl), cl[0], &cl, nullptr);
     }
 
     void constraint_manager::unwatch(clause& cl) {
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 87cb44a76..1d93c0cb2 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -155,7 +155,7 @@ namespace polysat {
         else if (c.is_always_false())
             m_conflict.set(c);
         else
-            propagate_bool_at(m_level, c.blit(), c->unit_clause());
+            assign_bool(m_level, c.blit(), c->unit_clause(), nullptr);
     }
 
     bool solver::can_propagate() {
@@ -178,6 +178,39 @@ namespace polysat {
         SASSERT(assignment_invariant());
     }
 
+    /**
+    * Propagate assignment to a Boolean variable
+    */
+    void solver::propagate(sat::literal lit) {
+        LOG_H2("Propagate bool " << lit);
+        signed_constraint c = lit2cnstr(lit);
+        SASSERT(c);
+        activate_constraint(c);
+        auto& wlist = m_bvars.watch(~lit);
+        unsigned i = 0, j = 0, sz = wlist.size();
+        for (; i < sz && !is_conflict(); ++i)
+            if (!propagate(lit, *wlist[i]))
+                wlist[j++] = wlist[i];
+        for (; i < sz; ++i)
+            wlist[j++] = wlist[i];
+        wlist.shrink(j);
+    }
+
+    /**
+    * Propagate assignment to a pvar
+    */
+    void solver::propagate(pvar v) {
+        LOG_H2("Propagate v" << v);
+        auto& wlist = m_pwatch[v];
+        unsigned i = 0, j = 0, sz = wlist.size();
+        for (; i < sz && !is_conflict(); ++i)
+            if (!wlist[i].propagate(*this, v))
+                wlist[j++] = wlist[i];
+        for (; i < sz; ++i)
+            wlist[j++] = wlist[i];
+        wlist.shrink(j);
+    }
+
     bool solver::propagate(sat::literal lit, clause& cl) {
         SASSERT(cl.size() >= 2);
         unsigned idx = cl[0] == ~lit ? 1 : 0;
@@ -210,39 +243,6 @@ namespace polysat {
 #endif
     }
 
-    /**
-    * Propagate assignment to a Boolean variable
-    */
-    void solver::propagate(sat::literal lit) {
-        LOG_H2("Propagate bool " << lit);
-        signed_constraint c = lit2cnstr(lit);
-        SASSERT(c);
-        activate_constraint(c);
-        auto& wlist = m_bvars.watch(~lit);
-        unsigned i = 0, j = 0, sz = wlist.size();
-        for (; i < sz && !is_conflict(); ++i)
-            if (!propagate(lit, *wlist[i]))
-                wlist[j++] = wlist[i];
-        for (; i < sz; ++i)
-            wlist[j++] = wlist[i];
-        wlist.shrink(j);
-    }
-
-    /**
-    * Propagate assignment to a pvar
-    */
-    void solver::propagate(pvar v) {
-        LOG_H2("Propagate v" << v);
-        auto& wlist = m_pwatch[v];
-        unsigned i = 0, j = 0, sz = wlist.size();
-        for (; i < sz && !is_conflict(); ++i) 
-            if (!wlist[i].propagate(*this, v))
-                wlist[j++] = wlist[i];
-        for (; i < sz; ++i)
-            wlist[j++] = wlist[i];
-        wlist.shrink(j);
-    }
-
     void solver::propagate(pvar v, rational const& val, signed_constraint c) {
         LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c);
         if (m_viable.is_viable(v, val)) {
@@ -587,7 +587,7 @@ namespace polysat {
         push_cjust(lemma.justified_var(), c);
 
         if (num_choices == 1)
-            propagate_bool_at(level(lemma), choice, &lemma);
+            assign_bool(level(lemma), choice, &lemma, nullptr);
         else
             decide_bool(choice, &lemma);
     }
@@ -681,19 +681,10 @@ namespace polysat {
     void solver::decide_bool(sat::literal lit, clause* lemma) {
         SASSERT(!can_propagate());
         SASSERT(!is_conflict());
-        push_level();
-        LOG_H2("Decide boolean literal " << lit << " @ " << m_level);
+        push_level();        
         assign_bool(m_level, lit, nullptr, lemma);
     }
 
-
-    void solver::propagate_bool_at(unsigned level, sat::literal lit, clause* reason) {
-        LOG("Propagate boolean literal " << lit << " @ " << level << " by " << show_deref(reason));
-        SASSERT(reason);
-        SASSERT(level <= m_level);
-        assign_bool(level, lit, reason, nullptr);
-    }
-
     unsigned solver::level(clause const& cl) {
         unsigned lvl = 0;
         for (auto lit : cl) {
@@ -707,7 +698,11 @@ namespace polysat {
     /// Assign a boolean literal and put it on the search stack
     void solver::assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma) {
         SASSERT(!m_bvars.is_true(lit));
-        LOG("Assigning boolean literal: " << lit);
+        if (reason)
+            LOG("Propagate literal " << lit << " @ " << level << " by " << *reason);
+        else
+            LOG("Decide literal " << lit << " @ " << m_level);
+        
         m_bvars.assign(lit, level, reason, lemma);
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 4c37be161..22becc979 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -153,7 +153,6 @@ namespace polysat {
         void deactivate_constraint(signed_constraint c);
         void decide_bool(clause& lemma);
         void decide_bool(sat::literal lit, clause* lemma);
-        void propagate_bool_at(unsigned level, sat::literal lit, clause* reason);
         unsigned level(clause const& cl);
 
         void assign_core(pvar v, rational const& val, justification const& j);