diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index ce7d34d4c..722a6f390 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -718,12 +718,7 @@ namespace polysat {
     void solver::backjump_lemma() {
         clause_ref lemma = m_conflict.build_lemma();
         LOG_H2("backjump_lemma: " << show_deref(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));
-        }
+        SASSERT(lemma && lemma_invariant(*lemma));
 
         // find second-highest level of the literals in the lemma
         unsigned max_level = 0;
@@ -821,6 +816,8 @@ namespace polysat {
         SASSERT(m_justification[v].is_decision());
 
         clause_ref lemma = m_conflict.build_lemma();
+        SASSERT(lemma && lemma_invariant(*lemma));
+
         if (lemma->empty())
             report_unsat();
         else {
@@ -830,6 +827,15 @@ namespace polysat {
         }
     }
 
+    bool solver::lemma_invariant(clause const& 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));
+        }
+        return true;
+    }
+
     unsigned solver::level(sat::literal lit0, clause const& cl) {
         unsigned lvl = 0;
         for (auto lit : cl) {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index bc6fb4582..38e55b471 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -227,6 +227,7 @@ namespace polysat {
 
         bool invariant();
         static bool invariant(signed_constraints const& cs);
+        bool lemma_invariant(clause const& lemma);
         bool wlist_invariant();
         bool assignment_invariant();
         bool verify_sat();