diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h
index 7b0783715..af5b883d6 100644
--- a/src/math/polysat/clause.h
+++ b/src/math/polysat/clause.h
@@ -35,6 +35,7 @@ namespace polysat {
 
         unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
         bool m_redundant = redundant_default;
+        bool m_active = false;  // clause is active iff it has been added to the solver and boolean watchlists
         sat::literal_vector m_literals;
         char const* m_name = "";
 
@@ -53,6 +54,8 @@ namespace polysat {
             SASSERT(count(m_literals, sat::null_literal) == 0);
         }
 
+        void set_active() { m_active = true; }
+
     public:
         void inc_ref() { m_ref_count++; }
         void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
@@ -77,6 +80,8 @@ namespace polysat {
         void set_redundant(bool r) { m_redundant = r; }
         bool is_redundant() const { return m_redundant; }
 
+        bool is_active() const { return m_active; }
+
         void set_name(char const* name) { m_name = name; }
         char const* name() const { return m_name; }
     };
diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 4ccab9f07..60f6da8e6 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -216,7 +216,7 @@ namespace polysat {
         logger().begin_conflict();
     }
 
-    void conflict::init(clause const& cl) {
+    void conflict::init(clause& cl) {
         LOG("Conflict: clause " << cl);
         SASSERT(empty());
         m_level = s.m_level;
@@ -225,6 +225,14 @@ namespace polysat {
             SASSERT_EQ(c.bvalue(s), l_false);
             insert(~c);
         }
+
+        // NOTE: usually in SAT solving, the conflict clause has at least two false literals at the max level.
+        //       (otherwise, the last literal would have been propagated at an earlier level.)
+        //       This is not true if we add clauses on demand;
+        //       after backtracking we may have the case that the conflict clause has
+        //       exactly one undefined literal that must be propagated explicitly.
+        m_lemmas.push_back(&cl);
+
         SASSERT(!empty());
         logger().begin_conflict();
     }
@@ -330,6 +338,10 @@ namespace polysat {
         // TODO: pass to inference_logger (with name)
    }
 
+    void conflict::restore_lemma(clause_ref lemma) {
+        m_lemmas.push_back(std::move(lemma));
+    }
+
     void conflict::remove(signed_constraint c) {
         SASSERT(contains(c));
         m_literals.remove(c.blit().index());
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 958b7993b..7c0990310 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -131,7 +131,7 @@ namespace polysat {
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** boolean conflict with the given clause */
-        void init(clause const& cl);
+        void init(clause& cl);
         /** conflict because there is no viable value for the variable v, by interval reasoning */
         void init_by_viable_interval(pvar v);
         /** conflict because there is no viable value for the variable v, by fallback solver */
@@ -157,11 +157,14 @@ namespace polysat {
         /** Evaluate constraint under assignment and insert it into conflict state. */
         void insert_eval(signed_constraint c);
 
-        /** Add a side lemma to the conflict; to be learned in addition to the main lemma after conflict resolution finishes. */
+        /** Add a lemma to the conflict, to be added after conflict resolution */
         void add_lemma(char const* name, std::initializer_list<signed_constraint> cs);
         void add_lemma(char const* name, signed_constraint const* cs, size_t cs_len);
         void add_lemma(char const* name, clause_ref lemma);
 
+        /** Re-add a lemma to the conflict that we were unable to add after the previous conflict. */
+        void restore_lemma(clause_ref lemma);
+
         /** Remove c from core */
         void remove(signed_constraint c);
         void remove_var(pvar v);
diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index f05257600..4ba310bcf 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -69,9 +69,11 @@ namespace polysat {
         m_clauses[clause_level].push_back(cl);
     }
 
-    void constraint_manager::store(clause* cl, bool value_propagate) {
+    void constraint_manager::store(clause* cl) {
+        VERIFY(!cl->is_active());
         register_clause(cl);
-        watch(*cl, value_propagate);
+        watch(*cl);
+        cl->set_active();
     }
 
     // Release constraints at the given level and above.
@@ -137,12 +139,11 @@ namespace polysat {
         SASSERT(std::all_of(cl.begin() + 1, cl.end(), [&](auto lit) { return get_watch_level(lit) <= get_watch_level(cl[1]); }));
     }
 
-    void constraint_manager::watch(clause& cl, bool value_propagate) {
+    void constraint_manager::watch(clause& cl) {
         if (cl.empty())
             return;
 
-        if (value_propagate) {
-#if 1
+        {
             // First, try to bool-propagate.
             // Otherwise, we might get a clause-conflict and a missed propagation after resolving the conflict.
             // With this, we will get a constraint-conflict instead.
@@ -180,7 +181,6 @@ namespace polysat {
                     s.assign_eval(~lit);
                 }
             }
-#endif
         }
 
         if (cl.size() == 1) {
diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index dc484f92d..0cc9ba93b 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -75,7 +75,7 @@ namespace polysat {
         void gc_clauses();
 
         void normalize_watch(clause& cl);
-        void watch(clause& cl, bool value_propagate);
+        void watch(clause& cl);
         void unwatch(clause& cl);
 
         void register_clause(clause* cl);
@@ -90,7 +90,7 @@ namespace polysat {
         constraint_manager(solver& s);
         ~constraint_manager();
 
-        void store(clause* cl, bool value_propagate);
+        void store(clause* cl);
 
         /// Release clauses at the given level and above.
         void release_level(unsigned lvl);
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index c581d3e1f..db2aeacd9 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1019,22 +1019,28 @@ namespace polysat {
                 UNREACHABLE();
             }
             if (is_conflict()) {
-                // TODO: the remainder of the narrow_queue as well as the lemmas are forgotten.
-                //       should we just insert them into the new conflict to carry them along?
+                // The remainder of narrow_queue is forgotten at this point,
+                // but keep the lemmas for later.
+                for (clause* lemma : lemmas)
+                    m_conflict.restore_lemma(lemma);
                 return;
             }
         }
 
-        for (clause* lemma : lemmas) {
-            add_clause(*lemma);
+        for (auto it = lemmas.begin(); it != lemmas.end(); ++it) {
+            clause& lemma = **it;
+            if (!lemma.is_active())
+                add_clause(lemma);
+            else
+                propagate_clause(lemma);
             // NOTE: currently, the backjump level is an overapproximation,
             //       since the level of evaluated constraints may not be exact (see TODO in assign_eval).
             // For this reason, we may actually get a conflict at this point
             // (because the actual jump_level of the lemma may be lower that best_level.)
             if (is_conflict()) {
-                // until this is fixed (if possible; and there may be other causes of conflict at this point),
-                // we just forget about the remaining lemmas and restart conflict analysis.
-                // TODO: we could also insert the remaining lemmas into the conflict and keep them for later.
+                // Keep the remaining lemmas for later.
+                for (; it != lemmas.end(); ++it)
+                    m_conflict.restore_lemma(*it);
                 return;
             }
         }
@@ -1063,6 +1069,24 @@ namespace polysat {
         }
     }  // backjump_and_learn
 
+    // Explicit boolean propagation over the given clause, without relying on watch lists
+    void solver::propagate_clause(clause& cl) {
+        sat::literal prop = sat::null_literal;
+        for (sat::literal lit : cl) {
+            if (m_bvars.is_true(lit))
+                return;  // clause is true
+            if (m_bvars.is_false(lit))
+                continue;
+            SASSERT(!m_bvars.is_assigned(lit));
+            if (prop != sat::null_literal)
+                return;  // two or more undef literals
+            prop = lit;
+        }
+        if (prop == sat::null_literal)
+            return;
+        assign_propagate(prop, cl);
+    }
+
     unsigned solver::level(sat::literal lit0, clause const& cl) {
         unsigned lvl = 0;
         for (auto lit : cl) {
@@ -1174,6 +1198,7 @@ namespace polysat {
         LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
         for (sat::literal lit : clause) {
             LOG("   " << lit_pp(*this, lit));
+            // TODO: move into constraint_manager::watch
             if (!m_bvars.is_assigned(lit)) {
                 switch (lit2cnstr(lit).eval(*this)) {
                 case l_true:
@@ -1190,12 +1215,11 @@ namespace polysat {
             if (m_bvars.value(lit) == l_true) {
                 // in this case the clause is useless
                 LOG("   Clause is already true, skipping...");
-                // SASSERT(false);  // should never happen (at least for redundant clauses)
                 return;
             }
         }
         SASSERT(!clause.empty());
-        m_constraints.store(&clause, true);
+        m_constraints.store(&clause);
 
         // Defer add_pwatch until the next solver iteration, because during propagation of a variable v the watchlist for v is locked.
         // NOTE: for non-redundant clauses, pwatching its constraints is required for soundness.
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index d6931e665..eb03fff2d 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -253,6 +253,8 @@ namespace polysat {
         void erase_pwatch(pvar v, constraint* c);
         void erase_pwatch(constraint* c);
 
+        void propagate_clause(clause& cl);
+
         void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }