From eba59356f3de8ca7fcc46defe3c4634996ed24d2 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 31 Oct 2022 15:17:32 +0100
Subject: [PATCH] Disable problematic resolve_with_assignment

---
 src/math/polysat/conflict.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index d8494413a..4ad1069b9 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -429,6 +429,7 @@ namespace polysat {
         // The reason for lit is conceptually:
         //    x1 = v1 /\ ... /\ xn = vn ==> lit
 
+        SASSERT(s.m_bvars.is_value_propagation(lit));
         SASSERT(contains(lit));
         SASSERT(!contains(~lit));
 
@@ -441,9 +442,12 @@ namespace polysat {
         // If evaluation depends on a decision,
         // then we rather keep the more general constraint c instead of inserting "x = v"
         bool has_decision = false;
+#if 0
+        // TODO: this is problematic; may skip relevant decisions
         for (pvar v : c->vars())
             if (s.is_assigned(v) && s.m_justification[v].is_decision())
                 m_bail_vars.insert(v), has_decision = true;
+#endif
 
         if (!has_decision) {
             remove(c);
@@ -452,6 +456,9 @@ namespace polysat {
                     m_vars.insert(v);
         }
 
+        SASSERT(!contains(lit));
+        SASSERT(!contains(~lit));
+
         logger().log(inf_resolve_with_assignment(s, lit, c));
     }