From 93410ccd81dce2bdbb56213f204dd9004310efac Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 23 Jan 2022 11:35:01 +0100
Subject: [PATCH] add assertion back for failing unit test, add comment about
 what is the bug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/explain.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 34064d735..cbc7d4040 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -92,7 +92,6 @@ namespace polysat {
             // c alone (+ variables) is now enough to represent the conflict.
             core.reset();
             core.set(c);
-            std::cout << "set c\n";
             return c->contains_var(v) ? l_undef : l_true;
         }
         return l_false;