From 3c093e03cffda63ad150290ab9b43c91fa73a011 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 22 Aug 2022 12:46:47 +0200
Subject: [PATCH] log

---
 src/math/polysat/solver.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 25c62e78e..0c974a88a 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -624,7 +624,7 @@ namespace polysat {
             return;
         }
         m_conflict.begin_conflict("resolve_conflict");
-        
+
         search_iterator search_it(m_search);
         while (search_it.next()) {
             auto& item = *search_it;
@@ -675,6 +675,7 @@ namespace polysat {
                 }
             }
         }
+        LOG("End of resolve_conflict loop");
         m_conflict.end_conflict();
         report_unsat();
     }
@@ -688,6 +689,11 @@ namespace polysat {
         clause_ref lemma = m_conflict.build_lemma().build();
         LOG_H2("backtrack_lemma: " << show_deref(lemma));
         SASSERT(lemma);
+        LOG("Lemma: " << *lemma);
+        for (sat::literal lit : *lemma) {
+            LOG("   Literal " << lit << " is: " << lit_pp(*this, lit));
+            SASSERT(m_bvars.value(lit) == l_false || lit2cnstr(lit).is_currently_false(*this));
+        }
 
         // find second-highest level of the literals in the lemma
         unsigned max_level = 0;  // could be simplified if we're sure that always max_level == m_level