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);
     }