From 8103627e477bc69e0647da35eac481eadae65dc1 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 14 Sep 2021 14:39:41 +0200
Subject: [PATCH] fix test_l4

---
 src/math/polysat/conflict_core.cpp | 3 ++-
 src/math/polysat/solver.cpp        | 4 +++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp
index 529ff4491..83b6b82c3 100644
--- a/src/math/polysat/conflict_core.cpp
+++ b/src/math/polysat/conflict_core.cpp
@@ -82,6 +82,7 @@ namespace polysat {
         for (auto v : c->vars())
             if (s().is_assigned(v))
                 m_vars.insert(v);
+        SASSERT(!empty());
     }
 
     /**
@@ -102,6 +103,7 @@ namespace polysat {
                 if (s().is_assigned(v))
                     m_vars.insert(v);
         }
+        SASSERT(!empty());
     }
 
     void conflict_core::insert(signed_constraint c) {
@@ -110,7 +112,6 @@ namespace polysat {
         // (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology)
         if (c.is_always_true())
             return;
-        SASSERT(!c.is_always_false());
         if (c->is_marked())
             return;
         set_mark(c);
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 0c1649422..a893660d5 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -178,7 +178,9 @@ namespace polysat {
         SASSERT(!is_conflict());
         SASSERT(c->unit_clause());
         if (c.bvalue(*this) == l_false)
-            m_conflict.set(c);  // we already added ~c => conflict at base level
+            m_conflict.set(~c);  // we already added ~c => conflict
+        else if (c.is_always_false())
+            m_conflict.set(c);
         else
             propagate_bool(c.blit(), c->unit_clause());
     }