From 06feb71eb1244353bd955de4f9e857752de4d3bb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Jan 2022 10:55:27 +0100
Subject: [PATCH] fix bug in root setting exposed by incremental mode pb_solver

---
 src/sat/sat_elim_eqs.cpp   |  7 ++++---
 src/sat/smt/euf_solver.cpp |  9 ++++++---
 src/sat/smt/pb_solver.cpp  | 14 ++++++++------
 3 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 928e84ebe..9bd42f1df 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -229,11 +229,12 @@ namespace sat {
             literal r  = roots[v];
             SASSERT(v != r.var());
 
-            if (m_solver.m_cut_simplifier) m_solver.m_cut_simplifier->set_root(v, r);
+            if (m_solver.m_cut_simplifier)
+                m_solver.m_cut_simplifier->set_root(v, r);
+
             bool set_root = m_solver.set_root(l, r);
-            bool root_ok = !m_solver.is_external(v) || set_root;
             TRACE("elim_eqs", tout << l << " " << r << "\n";);
-            if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
+            if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !set_root))) {
                 // cannot really eliminate v, since we have to notify extension of future assignments
                 if (m_solver.m_config.m_drat) {
                     m_solver.m_drat.add(~l, r, sat::status::redundant());
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index c057541b8..6aa12bc10 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -808,13 +808,16 @@ namespace euf {
     bool solver::set_root(literal l, literal r) {
         if (m_relevancy.enabled())
             return false;
-        expr* e = bool_var2expr(l.var());
-        if (!e)
-            return true;
         bool ok = true;
         for (auto* s : m_solvers)
             if (!s->set_root(l, r))
                 ok = false;
+
+        if (!ok)
+            return false;
+        expr* e = bool_var2expr(l.var());
+        if (!e)
+            return true;
         if (m.is_eq(e) && !m.is_iff(e))
             ok = false;
         euf::enode* n = get_enode(e);
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index 69920342d..5c67a05c5 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -2193,12 +2193,13 @@ namespace pb {
     }
 
     bool solver::set_root(literal l, literal r) { 
-        if (s().is_assumption(l.var())) {
+        if (s().is_assumption(l.var())) 
             return false;
-        }
         reserve_roots();
         m_roots[l.index()] = r;
         m_roots[(~l).index()] = ~r;
+        m_roots[r.index()] = r;
+        m_roots[(~r).index()] = ~r;
         m_root_vars[l.var()] = true;
         return true;
     }
@@ -2214,7 +2215,6 @@ namespace pb {
             flush_roots(*m_learned[i]);
         cleanup_constraints();
         // validate();
-
         // validate_eliminated();
     }
 
@@ -2225,7 +2225,8 @@ namespace pb {
 
     void solver::validate_eliminated(ptr_vector<constraint> const& cs) {
         for (constraint const* c : cs) {
-            if (c->learned()) continue;
+            if (c->learned())
+                continue;
             for (auto l : constraint::literal_iterator(*c))
                 VERIFY(!s().was_eliminated(l.var()));
         }
@@ -2449,9 +2450,10 @@ namespace pb {
         for (unsigned i = 0; !found && i < c.size(); ++i) {
             found = m_root_vars[c.get_lit(i).var()];
         }
-        if (!found) return;
+        if (!found)
+            return;
         clear_watch(c);
-        
+
         // this could create duplicate literals
         for (unsigned i = 0; i < c.size(); ++i) {
             literal lit = m_roots[c.get_lit(i).index()];