From eec153bb574a65cd1d0ce1ca7166b2c918e7a7b6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Dec 2019 14:49:58 +0100
Subject: [PATCH] fix #2779

---
 src/qe/qsat.cpp                 |  1 +
 src/smt/diff_logic.h            | 18 ++++++++++++++++++
 src/smt/theory_diff_logic_def.h |  3 +--
 src/smt/theory_utvpi_def.h      |  4 ++--
 4 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 0a016f82d..7fbb787fc 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -520,6 +520,7 @@ namespace qe {
             if ((m.is_true(val_a) && m.is_false(val_b)) || 
                 (m.is_false(val_a) && m.is_true(val_b))) {
                 TRACE("qe", 
+                      tout << model << "\n";
                       tout << mk_pp(a, m) << " := " << val_a << "\n";
                       tout << mk_pp(b, m) << " := " << val_b << "\n";
                       tout << m_elevel.find(a) << "\n";);
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index 89bc667e5..3e34dc6ca 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -915,6 +915,24 @@ public:
     // so the graph is disconnected.
     // assumption: the current assignment is feasible.
     //
+    void set_to_zero(unsigned n, dl_var const* vs) {
+        for (unsigned i = 0; i < n; ++i) {
+            dl_var v = vs[i];
+            if (!m_assignment[v].is_zero()) {
+                set_to_zero(v);
+                for (unsigned j = 0; j < n; ++j) {
+                    dl_var w = vs[j];
+                    if (!m_assignment[w].is_zero()) {
+                        enable_edge(add_edge(v, w, numeral(0), explanation()));
+                        enable_edge(add_edge(w, v, numeral(0), explanation()));
+                        SASSERT(is_feasible());                        
+                    }
+                }
+                return;
+            }
+        }
+    }
+
     void set_to_zero(dl_var v, dl_var w) {
         if (!m_assignment[v].is_zero()) {
             set_to_zero(v);
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 5e21792f6..1e961d1a9 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -360,8 +360,7 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
 
     TRACE("arith_final", display(tout); );
     // either will already be zero (as we don't do mixed constraints).
-    m_graph.set_to_zero(get_zero(true));
-    m_graph.set_to_zero(get_zero(false));
+    m_graph.set_to_zero(get_zero(true), get_zero(false));
     SASSERT(is_consistent());
     if (m_non_diff_logic_exprs) {
         return FC_GIVEUP; 
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 046a464c9..5612bc7c7 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -786,8 +786,8 @@ namespace smt {
         m.register_factory(m_factory);
         enforce_parity();
         init_zero();
-        m_graph.set_to_zero(to_var(m_izero), neg(to_var(m_izero)));
-        m_graph.set_to_zero(to_var(m_rzero), neg(to_var(m_rzero)));
+        dl_var vs[4] = { to_var(m_izero), neg(to_var(m_izero)), to_var(m_rzero), neg(to_var(m_rzero)) };
+        m_graph.set_to_zero(4, vs);
         compute_delta();   
         DEBUG_CODE(model_validate(););
     }