From f34e55e86ed6b504ba65543c0dd159dccc589223 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 8 Jan 2024 20:44:30 -0800
Subject: [PATCH] bugfix

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/polysat/core.cpp | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index a359ae123..6dd4479c4 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -358,7 +358,7 @@ namespace polysat {
 
     void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
         TRACE("bv", tout << "propagate assignment v" << v << " := " << value << "\n");
-        
+        SASSERT(!is_assigned(v));
         m_values[v] = value;
         m_justification[v] = dep;   
         m_assignment.push(v , value);
@@ -390,12 +390,18 @@ namespace polysat {
             // will not update m_watch[v] (other than copy constructor for m_watch)
             // because v has been assigned a value.
             propagate_eval({ idx });
-            if (s.inconsistent())
-                return;
+
            
             SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1])));
             if (!swapped)
                 m_watch[v][j++] = idx;
+            if (s.inconsistent()) {
+                ++k;
+                for (; k < sz; ++k)
+                    m_watch[v][j++] = m_watch[v][k];
+                m_watch[v].shrink(j);
+                return;
+            }
             if (vars.size() <= 1)
                 continue;
             auto v0 = vars[0];