From 4148ee128cbe4cbbc4dd57ac05c4fc4887a7570c Mon Sep 17 00:00:00 2001
From: Bernhard Gleiss <bgleiss@forsyte.tuwien.ac.at>
Date: Thu, 12 Oct 2017 16:05:31 +0200
Subject: [PATCH] fixed bug, which added too many edges between super-source
 and source in the case where the source was used by multiple inferences

---
 src/muz/spacer/spacer_unsat_core_plugin.cpp | 18 ++++++++++++++----
 src/muz/spacer/spacer_unsat_core_plugin.h   |  1 +
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index a1a937de0..0323fff0a 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -707,6 +707,8 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
      */
     void unsat_core_plugin_min_cut::add_edge(proof* i, proof* j)
     {
+        SASSERT(i != nullptr || j != nullptr);
+        
         unsigned node_i;
         unsigned node_j;
         if (i == nullptr)
@@ -735,7 +737,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
                 m_node_to_formula[node_other] = m.get_fact(i);
                 m_node_to_formula[node_i] = m.get_fact(i);
 
-                m_min_cut.add_edge(node_other, node_i);
+                m_min_cut.add_edge(node_other, node_i, 1);
             }
         }
 
@@ -765,12 +767,20 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
                 m_node_to_formula[node_j] = m.get_fact(j);
                 m_node_to_formula[node_other] = m.get_fact(j);
 
-                m_min_cut.add_edge(node_j, node_other);
+                m_min_cut.add_edge(node_j, node_other, 1);
             }
         }
 
-        // finally connect nodes
-        m_min_cut.add_edge(node_i, node_j);
+        // finally connect nodes (if there is not already a connection i -> j (only relevant if i is the supersource))
+        if (!(i == nullptr && m_connected_to_s.is_marked(j)))
+        {
+            m_min_cut.add_edge(node_i, node_j, 1);
+        }
+        
+        if (i == nullptr)
+        {
+            m_connected_to_s.mark(j, true);
+        }
     }
 
     /*
diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h
index 2ea4b4b51..6b679f3f2 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.h
+++ b/src/muz/spacer/spacer_unsat_core_plugin.h
@@ -108,6 +108,7 @@ private:
         void add_edge(proof* i, proof* j);
 
         vector<expr*> m_node_to_formula; // maps each node to the corresponding formula in the original proof
+        ast_mark m_connected_to_s; // remember which nodes have already been connected to the supersource, in order to avoid multiple edges.
 
         min_cut m_min_cut;
     };