From c79a16db2a687a6880cfdb7b2b72095cf24f6a6f Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 6 Feb 2023 16:28:41 +0100
Subject: [PATCH] Fix dependency tracking for input boolean conflicts

---
 src/math/polysat/solver.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b1f72f3a0..0ba926cf0 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -153,12 +153,13 @@ namespace polysat {
         if (is_conflict())
             return;  // no need to do anything if we already have a conflict at base level
         sat::literal lit = c.blit();
-        LOG("New constraint: " << lit_pp(*this, c));
+        LOG("New constraint " << c << " for " << dep);
         switch (m_bvars.value(lit)) {
         case l_false:
             // Input literal contradicts current boolean state (e.g., opposite literals in the input)
             // => conflict only flags the inconsistency
             set_conflict_at_base_level(dep);
+            m_conflict.insert(~c);  // ~c is true in the solver, need to track its original dependencies
             return;
         case l_true:
             // constraint c is already asserted => ignore
@@ -172,7 +173,6 @@ namespace polysat {
         switch (c.eval()) {
         case l_false:
             // asserted an always-false constraint => conflict at base level
-            LOG("Always false: " << c);
             set_conflict_at_base_level(dep);
             return;
         case l_true: