From b92f0acae32e9248a3d240f1e08d9468278284d2 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@microsoft.com>
Date: Thu, 18 May 2017 10:56:50 -0700
Subject: [PATCH] fix add_constraint and substitute_terms_in_linear_expression

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
---
 src/test/lp/lp.cpp              |  7 +++++++
 src/util/lp/init_lar_solver.cpp | 12 ------------
 src/util/lp/lar_solver.cpp      |  3 ---
 3 files changed, 7 insertions(+), 15 deletions(-)

diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 1acf4ba2a..3f9e2a4ce 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -2705,9 +2705,16 @@ void test_term() {
     ls.push_back(std::pair<mpq, var_index>((int)1, z));
     
     solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0));
+    ls.clear();
+    ls.push_back(std::pair<mpq, var_index>((int)1, x));
+    solver.add_constraint(ls, lconstraint_kind::LT, mpq(0));
+    ls.push_back(std::pair<mpq, var_index>((int)2, y));
+    solver.add_constraint(ls, lconstraint_kind::GT, mpq(0));
     auto status = solver.solve();
     std::cout << lp_status_to_string(status) << std::endl;
     std::unordered_map<var_index, mpq> model;
+    if (status != OPTIMAL)
+        return;
     solver.get_model(model);
     
     for (auto & t : model) {
diff --git a/src/util/lp/init_lar_solver.cpp b/src/util/lp/init_lar_solver.cpp
index 58486e6ba..a410d04ae 100644
--- a/src/util/lp/init_lar_solver.cpp
+++ b/src/util/lp/init_lar_solver.cpp
@@ -204,24 +204,12 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k
 }
 
 constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
-    this->print_linear_combination_of_column_indices(left_side_with_terms, std::cout);
-    std::cout << std::endl;
     vector<std::pair<mpq, var_index>> left_side;
     mpq rs = - right_side_parm;
-    std::cout << "before rs = " << rs << std::endl;
     substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs);
-    std::cout << "after rs = " << rs << std::endl;
-    
-    this->print_linear_combination_of_column_indices(left_side, std::cout);
-    std::cout << std::endl;
-    
     unsigned term_index = add_term(left_side, zero_of_type<mpq>());
     constraint_index ci = m_constraints.size();
     add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci);
-    std::cout << "constraint = ";
-    print_constraint(ci, std::cout);
-    std::cout << std::endl;
-
     return ci;
 }
 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 78b71ecfd..32c41b23e 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -557,9 +557,6 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
             register_one_coeff_in_map(coeffs, t.first, j);
         } else {
             const lar_term & term = * m_terms[adjust_term_index(t.second)];
-            std::cout << "term = ";
-            print_term(term, std::cout);
-            std::cout << std::endl;
             for (auto & p : term.coeffs()){
                 register_one_coeff_in_map(coeffs, t.first * p.second , p.first);
             }