From dcda39e76e68fd2264e681c42fb3ae25e10e3ade Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 19 Sep 2018 17:12:32 -0700
Subject: [PATCH] merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/lp/gomory.cpp   | 15 ++++++++++++---
 src/util/lp/lar_solver.h |  4 +---
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp
index 2dd349354..2136f5f3e 100644
--- a/src/util/lp/gomory.cpp
+++ b/src/util/lp/gomory.cpp
@@ -197,12 +197,21 @@ class gomory::imp {
         out << "(assert ( = ( +";
         dump_row_coefficients(out) << ") 0))\n";
     }
+
+    void dump_declaration(std::ostream& out, unsigned v) const {
+        out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n";
+    }
     
     void dump_declarations(std::ostream& out) const {
         // for a column j the var name is vj
         for (const auto & p : m_row) {
-            out << "(declare-const " << var_name(p.var()) 
-                << (is_int(p.var())? " Int" : " Real") << ")\n";
+            dump_declaration(out, p.var());
+        }
+        for (const auto& p : m_t) {
+            unsigned v = p.var();
+            if (m_int_solver.m_lar_solver->is_term(v)) {
+                dump_declaration(out, v);
+            }
         }
     }
 
@@ -298,7 +307,7 @@ public:
         lp_assert(m_int_solver.current_solution_is_inf_on_cut());
         TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
         m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k);
-        // TBD: validate result of subs_term_columns
+        TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
         TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
         return lia_move::cut;
     }
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 3c0ed4fbf..9e9edacc8 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -239,8 +239,7 @@ public:
 
     void analyze_new_bounds_on_row_tableau(
         unsigned row_index,
-        bound_propagator & bp
-                                           );
+        bound_propagator & bp);
 
     
     void substitute_basis_var_in_terms_for_row(unsigned i);
@@ -549,7 +548,6 @@ public:
             mpq v = it->second;
             t.m_coeffs.erase(it);
             t.m_coeffs[p.second] = v;
-            if (lt.m_v.is_zero()) continue;
             rs -= v * lt.m_v;
         }
     }