From 07d1f8657564ca930f7ac76699fafac6517aed54 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Sun, 12 Mar 2023 16:27:05 +0100
Subject: [PATCH] cleanup conflict::init and promote assertion

---
 src/math/polysat/conflict.cpp | 25 +++++++++----------------
 1 file changed, 9 insertions(+), 16 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 8116283df..6e052f3d8 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -199,20 +199,10 @@ namespace polysat {
         SASSERT(empty());
         m_level = s.m_level;
         m_narrow_queue.push_back(c.blit());  // if the conflict is only due to a missed propagation of c
-        if (c.bvalue(s) == l_false) {
-            // boolean conflict
-            // This case should not happen:
-            // - opposite input literals are handled separately
-            // - other boolean conflicts will discover violated clause during boolean propagation
-            VERIFY(false);  // fail here to force check when we encounter this case
-        }
-        else {
-            // Constraint c conflicts with the variable assignment
-            SASSERT_EQ(c.bvalue(s), l_true);
-            SASSERT(c.is_currently_false(s));
-            insert(c);
-            insert_vars(c);
-        }
+        VERIFY_EQ(c.bvalue(s), l_true);
+        SASSERT(c.is_currently_false(s));
+        insert(c);
+        insert_vars(c);
         SASSERT(!empty());
         logger().begin_conflict();
     }
@@ -271,7 +261,7 @@ namespace polysat {
         if (c.is_always_true())  // TODO: caller should avoid this?
             return;
         LOG("Inserting " << lit_pp(s, c));
-        SASSERT_EQ(c.bvalue(s), l_true);
+        VERIFY_EQ(c.bvalue(s), l_true);
         SASSERT(!c.is_always_true());   // such constraints would be removed earlier
         SASSERT(!c.is_always_false());  // if we added c, the core would be a tautology
         SASSERT(!c->vars().empty());
@@ -307,8 +297,11 @@ namespace polysat {
         VERIFY(lemma);
 
         for (auto lit : *lemma)
-            if (s.m_bvars.is_true(lit))
+            if (s.m_bvars.is_true(lit)) {
                 verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
+                // for (sat::literal lit : *lemma)
+                //     verbose_stream() << "    " << lit_pp(s, lit) << "\n";
+            }
 
         s.m_simplify_clause.apply(*lemma);
         lemma->set_redundant(true);