diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index fac2b1f4d..d8c0e23e8 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -60,6 +60,11 @@ namespace polysat {
         // m_unused.push_back(var);
     }
 
+    bool bool_var_manager::invariant(sat::bool_var var) const {
+        SASSERT_EQ(value(var) == l_undef, m_kind[var] == kind_t::unassigned);
+        return true;
+    }
+
     void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) {
         LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason);
         assign(kind_t::bool_propagation, lit, lvl, &reason);
@@ -78,6 +83,12 @@ namespace polysat {
         SASSERT(is_assumption(lit));
     }
 
+    void bool_var_manager::decision(sat::literal lit, unsigned lvl) {
+        LOG("Decided " << lit << " @ " << lvl);
+        assign(kind_t::decision, lit, lvl, nullptr);
+        SASSERT(is_decision(lit));
+    }
+
     void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep) {
         SASSERT(!is_assigned(lit));
         SASSERT(k != kind_t::unassigned);
diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index d7a7b274a..ecba32abd 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -25,6 +25,7 @@ namespace polysat {
             bool_propagation,
             value_propagation,
             assumption,
+            decision,
         };
 
         svector<sat::bool_var>      m_unused;   // previously deleted variables that can be reused by new_var();
@@ -36,6 +37,8 @@ namespace polysat {
         vector<ptr_vector<clause>>  m_watch;    // watch list for literals into clauses
 
         void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep = null_dependency);
+        bool invariant(sat::bool_var var) const;
+        bool invariant(sat::literal lit) const { return invariant(lit.var()); }
 
     public:
         bool_var_manager() {}
@@ -46,13 +49,15 @@ namespace polysat {
         sat::bool_var new_var();
         void del_var(sat::bool_var var);
 
-        bool is_assigned(sat::bool_var var) const { return value(var) != l_undef; }
-        bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; }
-        bool is_assumption(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::assumption; }
+        bool is_assigned(sat::bool_var var) const { SASSERT(invariant(var)); return value(var) != l_undef; }
+        bool is_assigned(sat::literal lit) const { SASSERT(invariant(lit)); return value(lit) != l_undef; }
+        bool is_assumption(sat::bool_var var) const { SASSERT(invariant(var)); return m_kind[var] == kind_t::assumption; }
         bool is_assumption(sat::literal lit) const { return is_assumption(lit.var()); }
-        bool is_bool_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::bool_propagation; }
+        bool is_decision(sat::bool_var var) const { SASSERT(invariant(var)); return m_kind[var] == kind_t::decision; }
+        bool is_decision(sat::literal lit) const { return is_decision(lit.var()); }
+        bool is_bool_propagation(sat::bool_var var) const { SASSERT(invariant(var)); return m_kind[var] == kind_t::bool_propagation; }
         bool is_bool_propagation(sat::literal lit) const { return is_bool_propagation(lit.var()); }
-        bool is_value_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::value_propagation; }
+        bool is_value_propagation(sat::bool_var var) const { SASSERT(invariant(var)); return m_kind[var] == kind_t::value_propagation; }
         bool is_value_propagation(sat::literal lit) const { return is_value_propagation(lit.var()); }
         lbool value(sat::bool_var var) const { return value(sat::literal(var)); }
         lbool value(sat::literal lit) const { return m_value[lit.index()]; }
@@ -70,6 +75,8 @@ namespace polysat {
         void propagate(sat::literal lit, unsigned lvl, clause& reason);
         void eval(sat::literal lit, unsigned lvl);
         void assumption(sat::literal lit, unsigned lvl, dependency dep);
+        void decision(sat::literal lit, unsigned lvl);
+
         void unassign(sat::literal lit);
 
         std::ostream& display(std::ostream& out) const;
@@ -81,8 +88,10 @@ namespace polysat {
             case kind_t::bool_propagation: return out << "bool propagation";
             case kind_t::value_propagation: return out << "value propagation";
             case kind_t::assumption: return out << "assumption";
-            default: UNREACHABLE(); return out;
+            case kind_t::decision: return out << "decision";
             }
+            UNREACHABLE();
+            return out;
         }
     };
 
diff --git a/src/math/polysat/log_helper.h b/src/math/polysat/log_helper.h
index 359243618..0489127c7 100644
--- a/src/math/polysat/log_helper.h
+++ b/src/math/polysat/log_helper.h
@@ -17,11 +17,10 @@ Author:
 --*/
 #pragma once
 
-#include <iostream>
+#include <ostream>
 #include <sstream>
+#include <type_traits>
 #include <utility>
-#include "util/ref.h"
-#include "util/util.h"
 
 template <typename T>
 struct show_deref_t {
@@ -29,11 +28,11 @@ struct show_deref_t {
 };
 
 template <typename T>
-std::ostream& operator<<(std::ostream& os, show_deref_t<T> s) {
+std::ostream& operator<<(std::ostream& out, show_deref_t<T> s) {
     if (s.ptr)
-        return os << *s.ptr;
+        return out << *s.ptr;
     else
-        return os << "<null>";
+        return out << "<null>";
 }
 
 template <typename T>
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index be93ce36b..f2c5462e2 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -50,10 +50,13 @@ namespace polysat {
                     out << "\n\t" << rpad(4, l2) << ": " << rpad(16, s.lit2cnstr(l2)) << "   " << bool_justification_pp(s.m_bvars, l2);
                 }
             }
-            else {
-                SASSERT(s.m_bvars.is_value_propagation(lit));
+            else if (s.m_bvars.is_value_propagation(lit)) {
                 out << " evaluated";
             }
+            else {
+                SASSERT(s.m_bvars.is_decision(lit));
+                out << " decision";
+            }
             return out;
         }
         }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 051ce8372..67886cfff 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -495,6 +495,10 @@ namespace polysat {
                 pop_qhead();
                 break;
             }
+            case trail_instr_t::lemma_qhead_i: {
+                m_lemmas_qhead--;
+                break;
+            }
             case trail_instr_t::pwatch_i: {
                 constraint* c = m_pwatch_trail.back();
                 erase_pwatch(c);
@@ -561,10 +565,70 @@ namespace polysat {
         }
     }
 
+    bool solver::can_decide() const {
+        return can_pdecide() || can_bdecide();
+    }
+
+    bool solver::can_pdecide() const {
+        return !m_free_pvars.empty();
+    }
+
+    bool solver::can_bdecide() const {
+        return m_lemmas_qhead < m_lemmas.size();
+    }
+
     void solver::decide() {
         LOG_H2("Decide");
         SASSERT(can_decide());
-        pdecide(m_free_pvars.next_var());
+        SASSERT(can_pdecide());  // if !can_pdecide(), all boolean literals have been propagated...
+        if (can_bdecide())
+            bdecide();
+        else
+            pdecide(m_free_pvars.next_var());
+    }
+
+    /// Basic version of https://en.cppreference.com/w/cpp/experimental/scope_exit
+    template <typename Callable>
+    class on_scope_exit final {
+        Callable m_ef;
+    public:
+        explicit on_scope_exit(Callable&& ef)
+            : m_ef(std::forward<Callable>(ef))
+        { }
+        ~on_scope_exit() {
+            m_ef();
+        }
+    };
+
+    void solver::bdecide() {
+        clause& lemma = *m_lemmas[m_lemmas_qhead++];
+        on_scope_exit update_trail([this]() {
+            // must be done after push_level, but also if we return early.
+            m_trail.push_back(trail_instr_t::lemma_qhead_i);
+        });
+
+        LOG_H2("Decide on non-asserting lemma: " << lemma);
+        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
+                return;
+            case l_false:
+                break;
+            case l_undef:
+                if (choice == sat::null_literal)
+                    choice = lit;
+                break;
+            }
+        }
+        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.
+        push_level();
+        assign_decision(choice);
     }
 
     void solver::pdecide(pvar v) {
@@ -718,7 +782,7 @@ namespace polysat {
     void solver::backjump_lemma() {
         clause_ref lemma = m_conflict.build_lemma();
         LOG_H2("backjump_lemma: " << show_deref(lemma));
-        SASSERT(lemma && lemma_invariant(*lemma));
+        SASSERT(lemma_invariant(lemma.get()));
 
         // find second-highest level of the literals in the lemma
         unsigned max_level = 0;
@@ -795,8 +859,15 @@ namespace polysat {
         LOG("Learning: "<< lemma);
         SASSERT(!lemma.empty());
         m_simplify_clause.apply(lemma);
-        // TODO: print warning if the lemma is non-asserting?
         add_clause(lemma);
+        // At this point, all literals in lemma have been value- or bool-propated, if possible.
+        // So if the lemma is/was asserting, all its literals are now assigned.
+        bool is_asserting = all_of(lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); });
+        if (!is_asserting) {
+            LOG("Lemma is not asserting!");
+            m_lemmas.push_back(&lemma);
+            SASSERT(can_bdecide());
+        }
     }
 
     /**
@@ -816,7 +887,7 @@ namespace polysat {
         SASSERT(m_justification[v].is_decision());
 
         clause_ref lemma = m_conflict.build_lemma();
-        SASSERT(lemma && lemma_invariant(*lemma));
+        SASSERT(lemma_invariant(lemma.get()));
 
         if (lemma->empty())
             report_unsat();
@@ -827,9 +898,10 @@ namespace polysat {
         }
     }
 
-    bool solver::lemma_invariant(clause const& lemma) {
-        LOG("Lemma: " << lemma);
-        for (sat::literal lit : lemma) {
+    bool solver::lemma_invariant(clause const* lemma) {
+        SASSERT(lemma);
+        LOG("Lemma: " << *lemma);
+        for (sat::literal lit : *lemma) {
             LOG("  " << lit_pp(*this, lit));
             SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this));
         }
@@ -848,6 +920,12 @@ namespace polysat {
         return lvl;
     }
 
+    void solver::assign_decision(sat::literal lit) {
+        m_bvars.decision(lit, m_level);
+        m_trail.push_back(trail_instr_t::assign_bool_i);
+        m_search.push_boolean(lit);
+    }
+
     void solver::assign_propagate(sat::literal lit, clause& reason) {
         m_bvars.propagate(lit, level(lit, reason), reason);
         m_trail.push_back(trail_instr_t::assign_bool_i);
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 38e55b471..9b2ae4fc6 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -134,6 +134,9 @@ namespace polysat {
         unsigned_vector          m_qhead_trail;
         constraints              m_pwatch_trail;
 
+        ptr_vector<clause>       m_lemmas;  ///< the non-asserting lemmas
+        unsigned                 m_lemmas_qhead = 0;
+
         unsigned_vector          m_base_levels;  // External clients can push/pop scope. 
 
         void push_qhead() { 
@@ -163,7 +166,7 @@ namespace polysat {
         void pop_levels(unsigned num_levels);
 
         void assign_propagate(sat::literal lit, clause& reason);
-        void assign_decision(sat::literal lit, clause& lemma);
+        void assign_decision(sat::literal lit);
         void assign_eval(sat::literal lit);
         void activate_constraint(signed_constraint c);
         void deactivate_constraint(signed_constraint c);
@@ -190,8 +193,11 @@ namespace polysat {
         void set_conflict(clause& cl) { m_conflict.init(cl); }
         void set_conflict(pvar v, bool by_viable_fallback) { m_conflict.init(v, by_viable_fallback); }
 
-        bool can_decide() const { return !m_free_pvars.empty(); }
+        bool can_decide() const;
+        bool can_bdecide() const;
+        bool can_pdecide() const;
         void decide();
+        void bdecide();
         void pdecide(pvar v);
 
         void linear_propagate();
@@ -227,7 +233,7 @@ namespace polysat {
 
         bool invariant();
         static bool invariant(signed_constraints const& cs);
-        bool lemma_invariant(clause const& lemma);
+        bool lemma_invariant(clause const* lemma);
         bool wlist_invariant();
         bool assignment_invariant();
         bool verify_sat();
diff --git a/src/math/polysat/trail.h b/src/math/polysat/trail.h
index 08e04de1d..8411024c9 100644
--- a/src/math/polysat/trail.h
+++ b/src/math/polysat/trail.h
@@ -16,8 +16,9 @@ Author:
 
 namespace polysat {
 
-    enum class trail_instr_t { 
+    enum class trail_instr_t {
         qhead_i,
+        lemma_qhead_i,
         pwatch_i,
         add_var_i,
         inc_level_i,
@@ -28,6 +29,4 @@ namespace polysat {
         assign_bool_i
     };
 
-    
-
 }