diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp
index 1c26e7573..5233047ab 100644
--- a/src/math/polysat/clause_builder.cpp
+++ b/src/math/polysat/clause_builder.cpp
@@ -23,7 +23,6 @@ namespace polysat {
 
     void clause_builder::reset() {
         m_literals.reset();
-        m_new_constraints.reset();
         m_level = 0;
         m_dep = nullptr;
         SASSERT(empty());
@@ -42,23 +41,27 @@ namespace polysat {
     }
 
     void clause_builder::push_literal(sat::literal lit) {
-        constraint* c = m_solver.m_constraints.lookup(lit.var());
+        push(m_solver.m_constraints.lookup(lit));
+    }
+
+    void clause_builder::push(signed_constraint c) {
         SASSERT(c);
+        SASSERT(c->has_bvar());
         if (c->unit_clause()) {
-            add_dependency(c->unit_clause()->dep());
+            add_dependency(c->unit_dep());
             return;
         }
         m_level = std::max(m_level, c->level());
-        m_literals.push_back(lit);
+        m_literals.push_back(c.blit());
     }
 
-    void clause_builder::push_new_constraint(signed_constraint c) {
-        SASSERT(c);
-        if (c.is_always_false())
-            return;
-        m_level = std::max(m_level, c->level());
-        m_literals.push_back(c.blit());
-        m_new_constraints.push_back(c.get());
-    }
+    // void clause_builder::push_new_constraint(signed_constraint c) {
+    //     SASSERT(c);
+    //     if (c.is_always_false())
+    //         return;
+    //     m_level = std::max(m_level, c->level());
+    //     m_literals.push_back(c.blit());
+    //     m_new_constraints.push_back(c.get());
+    // }
 
 }
diff --git a/src/math/polysat/clause_builder.h b/src/math/polysat/clause_builder.h
index 40c358caa..84792da3e 100644
--- a/src/math/polysat/clause_builder.h
+++ b/src/math/polysat/clause_builder.h
@@ -27,16 +27,17 @@ namespace polysat {
     class clause_builder {
         solver&               m_solver;
         sat::literal_vector   m_literals;
-        scoped_ptr_vector<constraint> m_new_constraints;
         p_dependency_ref      m_dep;
         unsigned              m_level = 0;
 
     public:
         clause_builder(solver& s);
 
-        bool empty() const { return m_literals.empty() && m_new_constraints.empty() && m_dep == nullptr && m_level == 0; }
+        bool empty() const { return m_literals.empty() && m_dep == nullptr && m_level == 0; }
         void reset();
 
+        unsigned level() const { return m_level; }
+
         /// Build the clause. This will reset the clause builder so it can be reused.
         clause_ref build();
 
@@ -45,9 +46,15 @@ namespace polysat {
         /// Add a literal to the clause.
         /// Intended to be used for literals representing a constraint that already exists.
         void push_literal(sat::literal lit);
+
+        void push(signed_constraint c);
       
         /// Add a constraint to the clause that does not yet exist in the solver so far.
-        void push_new_constraint(signed_constraint c);
+        // void push_new_constraint(signed_constraint c);
+
+        using const_iterator = decltype(m_literals)::const_iterator;
+        const_iterator begin() const { return m_literals.begin(); }
+        const_iterator end() const { return m_literals.end(); }
     };
 
 }
diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp
index 92a786b94..b5cae383b 100644
--- a/src/math/polysat/conflict_core.cpp
+++ b/src/math/polysat/conflict_core.cpp
@@ -130,11 +130,40 @@ namespace polysat {
         m_solver->activate_constraint(c);
     }
 
-    clause_ref conflict_core::build_lemma(unsigned model_level) {
+    /** Create fallback lemma that excludes the current search state */
+    /**
+    * revisit: can prune literals further by slicing base on cone of influence
+    * based on marked literals/variables on the stack. Only decisions that affect
+    * marked items need to be included.
+    */
+    clause_builder conflict_core::build_fallback_lemma(unsigned lvl) {
+        LOG_H3("Creating fallback lemma for level " << lvl);
+        LOG_V("m_search: " << m_solver->m_search);
+        clause_builder lemma(*m_solver);
+        unsigned todo = lvl;
+        unsigned i = 0;
+        while (todo > 0) {
+            auto const& item = m_solver->m_search[i++];
+            if (!m_solver->is_decision(item))
+                continue;
+            LOG_V("Adding: " << item);
+            if (item.is_assignment()) {
+                pvar v = item.var();
+                auto c = ~cm().eq(0, m_solver->var(v) - m_solver->m_value[v]);
+                cm().ensure_bvar(c.get());
+                lemma.push_literal(c.blit());
+            } else {
+                sat::literal lit = item.lit();
+                lemma.push_literal(~lit);
+            }
+            --todo;
+        }
+        return lemma;
+    }
+
+    clause_builder conflict_core::build_core_lemma(unsigned model_level) {
         LOG_H3("build lemma from core");
-        sat::literal_vector literals;
-        p_dependency_ref dep = m_solver->mk_dep_ref(null_dependency);
-        unsigned lvl = 0;
+        clause_builder lemma(*m_solver);
 
         // TODO: try a final core reduction step?
 
@@ -146,12 +175,7 @@ namespace polysat {
                 // Insert the temporary constraint from saturation into \Gamma.
                 handle_saturation_premises(c);
             }
-            if (c->unit_clause()) {
-                dep = m_solver->m_dm.mk_join(dep, c->unit_dep());
-                continue;
-            }
-            lvl = std::max(lvl, c->level());
-            literals.push_back(~c.blit());
+            lemma.push(c);
         }
 
         if (m_needs_model) {
@@ -166,13 +190,20 @@ namespace polysat {
                 // SASSERT(!m_solver->m_justification[v].is_unassigned());  // TODO: why does this trigger????
                 if (m_solver->m_justification[v].level() > model_level)
                     continue;
-                auto diseq = ~cm().eq(lvl, m_solver->var(v) - m_solver->m_value[v]);
+                auto diseq = ~cm().eq(lemma.level(), m_solver->var(v) - m_solver->m_value[v]);
                 cm().ensure_bvar(diseq.get());
-                literals.push_back(diseq.blit());
+                lemma.push(diseq);
             }
         }
 
-        return clause::from_literals(lvl, std::move(dep), std::move(literals));
+        return lemma;
+    }
+
+    clause_builder conflict_core::build_lemma(unsigned reverted_level) {
+        if (is_bailout())
+            return build_fallback_lemma(reverted_level);
+        else
+            return build_core_lemma(reverted_level - 1);
     }
 
     bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict_core.h
index 0df48aa33..8bf72b13c 100644
--- a/src/math/polysat/conflict_core.h
+++ b/src/math/polysat/conflict_core.h
@@ -13,6 +13,7 @@ Author:
 --*/
 #pragma once
 #include "math/polysat/constraint.h"
+#include "math/polysat/clause_builder.h"
 
 namespace polysat {
 
@@ -89,7 +90,9 @@ namespace polysat {
         bool resolve_value(pvar v, vector<signed_constraint> const& cjust_v);
 
         /** Convert the core into a lemma to be learned. */
-        clause_ref build_lemma(unsigned model_level);
+        clause_builder build_lemma(unsigned reverted_level);
+        clause_builder build_core_lemma(unsigned model_level);
+        clause_builder build_fallback_lemma(unsigned lvl);
 
         bool try_eliminate(pvar v);
         bool try_saturate(pvar v);
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 38bf919e3..1a0057061 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -54,6 +54,7 @@ namespace polysat {
                 if (!c2.is_currently_false(s()))
                     continue;
 
+                // TODO: separate method for this; then try_explain1 and try_explain* for multi-steps; replace the false constraint in the core.
                 // c1 is true, c2 is false
                 LOG("c1: " << c1);
                 LOG("c2: " << c2);
@@ -71,7 +72,7 @@ namespace polysat {
                 premises.push_back(c1);
                 premises.push_back(c2);
                 if (!c->contains_var(v)) {
-                    core.reset();
+                    core.reset(); // TODO: doesn't work; this removes the premises as well... / instead: remove the false one.
                     core.insert(c, std::move(premises));
                     return true;
                 } else {
diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index fad048969..1e790dc5c 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -66,6 +66,9 @@ namespace polysat {
 
     bool forbidden_intervals::explain(solver& s, vector<signed_constraint> const& conflict, pvar v, clause_ref& out_lemma) {
 
+        return false;
+
+#if 0
         // Extract forbidden intervals from conflicting constraints
         vector<fi_record> records;
         bool has_full = false;
@@ -174,6 +177,7 @@ namespace polysat {
         }
         out_lemma = clause.build();
         return true;
+#endif
     }
 
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index eb645e24e..fa9ec5463 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -644,11 +644,7 @@ namespace polysat {
         SASSERT(m_justification[v].is_decision());
         unsigned const lvl = m_justification[v].level();
 
-        clause_ref lemma;
-        if (m_conflict.is_bailout())
-            lemma = mk_fallback_lemma(lvl);  // must call this before backjump
-        else
-            lemma = m_conflict.build_lemma(lvl - 1);
+        clause_ref lemma = m_conflict.build_lemma(lvl).build();
         m_conflict.reset();
 
         backjump(lvl - 1);
@@ -686,43 +682,11 @@ namespace polysat {
             return m_bvars.is_decision(item.lit().var());
     }
 
-    /** Create fallback lemma that excludes the current search state */
-    /**
-    * revisit: can prune literals further by slicing base on cone of influence
-    * based on marked literals/variables on the stack. Only decisions that affect
-    * marked items need to be included.
-    */
-    clause_ref solver::mk_fallback_lemma(unsigned lvl) {
-        LOG_H3("Creating fallback lemma for level " << lvl);
-        LOG_V("m_search: " << m_search);
-        clause_builder lemma(*this);
-        unsigned todo = lvl;
-        unsigned i = 0;
-        while (todo > 0) {
-            auto const& item = m_search[i++];
-            if (!is_decision(item))
-                continue;
-            LOG_V("Adding: " << item);
-            if (item.is_assignment()) {
-                pvar v = item.var();
-                auto c = ~m_constraints.eq(0, var(v) - m_value[v]);
-                m_constraints.ensure_bvar(c.get());
-                lemma.push_literal(c.blit());
-            } else {
-                sat::literal lit = item.lit();
-                lemma.push_literal(~lit);
-            }
-            --todo;
-        }
-        return lemma.build();
-    }
-
     void solver::revert_bool_decision(sat::literal lit) {
         sat::bool_var const var = lit.var();
         LOG_H3("Reverting boolean decision: " << lit);
         SASSERT(m_bvars.is_decision(var));
 
-        // TODO:
         // Current situation: we have a decision for boolean literal L on top of the stack, and a conflict core.
         //
         // In a CDCL solver, this means ~L is in the lemma (actually, as the asserting literal). We drop the decision and replace it by the propagation (~L)^lemma.
@@ -741,18 +705,14 @@ namespace polysat {
         //      again L is in core, unless we core-reduced it away
         unsigned const lvl = m_bvars.level(var);
 
-        clause_ref reason;
-        if (m_conflict.is_bailout())
-            reason = mk_fallback_lemma(lvl);
-        else
-            reason = m_conflict.build_lemma(lvl - 1);
+        clause_builder reason_builder = m_conflict.build_lemma(lvl);
         m_conflict.reset();
 
-        bool contains_lit = std::any_of(reason->begin(), reason->end(), [lit](auto reason_lit) { return reason_lit == ~lit; });
+        bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit);
+        // bool contains_lit = std::any_of(reason_builder->begin(), reason_builder->end(), [lit](auto reason_lit) { return reason_lit == ~lit; });
         if (!contains_lit) {
-            // Problem:
-            // a(x), b(x) => c(y)    [ i.e., a(x) no longer in the core ]
-            // but now what to do with decision a(x)^?
+            // At this point, we do not have ~lit in the reason.
+            // For now, we simply add it (thus weakening the reason)
             //
             // Alternative (to be considered later):
             // - 'reason' itself (without ~L) would already be an explanation for ~L
@@ -760,10 +720,10 @@ namespace polysat {
             // - would need to check what we can gain by relaxing that invariant
             // - drawback: might have to bail out at boolean resolution
             // Also: maybe we can skip ~L in some cases? but in that case it shouldn't be marked.
-            SASSERT(false); // debugging: just to find a case when this happens.
-            // lemma does not contain ~L, so we add it (thus weakening the lemma)
-            NOT_IMPLEMENTED_YET();  // should add it to the core before calling build_lemma.
+            //
+            reason_builder.push_literal(~lit);
         }
+        clause_ref reason = reason_builder.build();
 
         // The lemma where 'lit' comes from.
         // Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma.
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 1d66cfdb1..f9454f699 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -218,7 +218,6 @@ namespace polysat {
         void resolve_bool(sat::literal lit);
         void revert_decision(pvar v);
         void revert_bool_decision(sat::literal lit);
-        clause_ref mk_fallback_lemma(unsigned lvl);
 
         void report_unsat();
         void learn_lemma(pvar v, clause_ref lemma);