From be993485d0a72e751d1cd63f0ea02cfd47a5a638 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 24 Oct 2023 13:14:35 +0200
Subject: [PATCH] note non-false literals in clause

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

diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp
index 32eeed102..39f3d7fa3 100644
--- a/src/math/polysat/clause_builder.cpp
+++ b/src/math/polysat/clause_builder.cpp
@@ -89,6 +89,13 @@ namespace polysat {
     void clause_builder::insert_eval(signed_constraint c) {
         if (c.bvalue(*m_solver) == l_undef)
             m_solver->assign_eval(~c.blit());
+        if (c.bvalue(*m_solver) != l_false) {
+            IF_VERBOSE(1,
+                verbose_stream() << "clause_builder: " << (m_name ? m_name : "<null>") << "\n";
+                verbose_stream() << "    constraint is not b:false: " << lit_pp(*m_solver, c) << "\n";
+            );
+        }
+        // SASSERT_EQ(c.bvalue(*m_solver), l_false);
         insert(c);
     }