diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index 043ae8c5c..999297bd1 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -66,25 +66,25 @@ namespace polysat {
     }
 
     void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) {
-        LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason);
+        LOG("Propagate " << lit << " @ " << lvl << " by " << reason);
         assign(kind_t::bool_propagation, lit, lvl, &reason);
         SASSERT(is_bool_propagation(lit));
     }
 
     void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
-        LOG_V("Eval literal " << lit << " @ " << lvl);
+        LOG_V("Evaluate " << lit << " @ " << lvl);
         assign(kind_t::evaluation, lit, lvl, nullptr);
         SASSERT(is_evaluation(lit));
     }
 
     void bool_var_manager::assumption(sat::literal lit, unsigned lvl, dependency dep) {
-        LOG("Asserted " << lit << " @ " << lvl);
+        LOG("Assert " << lit << " @ " << lvl);
         assign(kind_t::assumption, lit, lvl, nullptr, dep);
         SASSERT(is_assumption(lit));
     }
 
     void bool_var_manager::decision(sat::literal lit, unsigned lvl) {
-        LOG("Decided " << lit << " @ " << lvl);
+        LOG("Decide " << lit << " @ " << lvl);
         assign(kind_t::decision, lit, lvl, nullptr);
         SASSERT(is_decision(lit));
     }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 0eb027e4f..42c9ea9e8 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -518,7 +518,6 @@ namespace polysat {
     void solver::decide() {
         LOG_H2("Decide");
         SASSERT(can_decide());
-        SASSERT(can_pdecide());  // if !can_pdecide(), all boolean literals have been propagated...
         if (can_bdecide())
             bdecide();
         else
@@ -533,11 +532,17 @@ namespace polysat {
         };
 
         LOG_H2("Decide on non-asserting lemma: " << lemma);
+        for (sat::literal lit : lemma) {
+            LOG(lit_pp(*this, lit));
+        }
         sat::literal choice = sat::null_literal;
         for (sat::literal lit : lemma) {
             switch (m_bvars.value(lit)) {
             case l_true:
                 // Clause is satisfied; nothing to do here
+                // Happens when all other branches of the lemma have been tried.
+                // The last branch is entered due to propagation, while the lemma is still on the stack as a decision point.
+                LOG("Skip decision (clause already satisfied)");
                 return;
             case l_false:
                 break;
@@ -548,10 +553,9 @@ namespace polysat {
             }
         }
         LOG("Choice is " << lit_pp(*this, choice));
-        // SASSERT(2 <= count_if(lemma, [this](sat::literal lit) { return !m_bvars.is_assigned(lit); });
         SASSERT(choice != sat::null_literal);
-        // TODO: is the case after backtracking correct?
-        //       => the backtracking code has to handle this. making sure that the decision literal is set to false.
+        SASSERT(2 <= count_if(lemma, [this](sat::literal lit) { return !m_bvars.is_assigned(lit); }));
+        SASSERT(can_pdecide());  // if !can_pdecide(), all boolean literals have been evaluated
         push_level();
         assign_decision(choice);
     }
@@ -950,7 +954,6 @@ namespace polysat {
                 LOG_H3("Main lemma is not asserting: " << *best_lemma);
                 for (sat::literal lit : *best_lemma) {
                     LOG(lit_pp(*this, lit));
-                    // SASSERT(m_bvars.value(lit) != l_true);
                 }
                 m_lemmas.push_back(best_lemma);
                 m_trail.push_back(trail_instr_t::add_lemma_i);