From cf80225feef63c1717b12239c315f1df2c7db151 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 13 Sep 2021 14:46:35 +0200
Subject: [PATCH] lemma

---
 src/math/polysat/conflict_core.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp
index b380eff43..070b98ff1 100644
--- a/src/math/polysat/conflict_core.cpp
+++ b/src/math/polysat/conflict_core.cpp
@@ -219,11 +219,13 @@ namespace polysat {
         clause_builder lemma(s());
 
         for (auto c : m_constraints) {
-            if (!c->has_bvar())
-                keep(c);
-            lemma.push(~c);
+            SASSERT(!c->has_bvar());
+            keep(c);
         }
 
+        for (auto c : *this)
+            lemma.push(~c);
+
         for (unsigned v : m_vars) {
             if (!is_pmarked(v))
                 continue;