From 879bb4b1f07da3b79fbc081235a710fc334c6a56 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 10 Nov 2024 19:35:01 -0800
Subject: [PATCH] avoid circular dependencies in justifications that get
 updated. fixes #7443

---
 src/sat/sat_solver.cpp | 12 ++++++------
 src/sat/sat_solver.h   |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e6d35659850..1f069e3cb8a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -518,12 +518,12 @@ namespace sat {
     }
 
     bool solver::propagate_bin_clause(literal l1, literal l2) {
-        if (value(l2) == l_false) {
+        if (value(l2) == l_false && value(l1) != l_true) {
             m_stats.m_bin_propagate++;
             assign(l1, justification(lvl(l2), l2));            
             return true;
         }
-        if (value(l1) == l_false) {
+        if (value(l1) == l_false && value(l2) != l_true) {
             m_stats.m_bin_propagate++;
             assign(l2, justification(lvl(l1), l1));
             return true;
@@ -4579,7 +4579,6 @@ namespace sat {
     void solver::extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed_vars, vector<literal_vector>& conseq) {
         for (literal lit: unfixed_lits) {
             TRACE("sat", tout << "extract: " << lit << " " << value(lit) << " " << lvl(lit) << "\n";);
-
             if (lvl(lit) <= 1 && value(lit) == l_true) {
                 extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
             }
@@ -4606,7 +4605,8 @@ namespace sat {
         case justification::NONE:
             break;
         case justification::BINARY:
-            if (!check_domain(lit, ~js.get_literal())) return false;
+            if (!check_domain(lit, ~js.get_literal())) 
+                return false;
             s |= m_antecedents.find(js.get_literal().var());
             break;
         case justification::CLAUSE: {
@@ -4680,9 +4680,9 @@ namespace sat {
         SASSERT(m_todo_antecedents.empty());
         m_todo_antecedents.push_back(lit);
         while (!m_todo_antecedents.empty()) {
-            if (extract_fixed_consequences1(m_todo_antecedents.back(), assumptions, unfixed, conseq)) {
+            auto lit = m_todo_antecedents.back();
+            if (extract_fixed_consequences1(lit, assumptions, unfixed, conseq)) 
                 m_todo_antecedents.pop_back();
-            }
         }
     }
 
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 2a150f4d9a1..a12a23a6f8a 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -406,7 +406,7 @@ namespace sat {
             }
         }
         void update_assign(literal l, justification j) {
-            if (j.level() == 0 && !m_trim) 
+            if (j.level() == 0 && !m_trim && lvl(l) != 0) 
                 m_justification[l.var()] = j;
         }
         void assign_unit(literal l) { assign(l, justification(0)); }