From a80eb134203ff1aafe64743c64eeaeb102f5f551 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sun, 8 Mar 2020 11:59:23 -0700
Subject: [PATCH] fixes in bound setting in cube, and in lar_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/lar_solver.cpp            | 14 ++++++++------
 src/math/lp/lar_solver.h              |  2 +-
 src/math/lp/lp_core_solver_base_def.h |  1 +
 3 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 89c518bf6..cd76023bd 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1781,17 +1781,19 @@ void lar_solver::activate(constraint_index ci) {
     update_column_type_and_bound(c.column(), c.kind(), c.rhs(), ci);
 }
 
-mpq lar_solver::adjust_bound_for_int(lpvar j, lconstraint_kind k, const mpq& bound) {
+mpq lar_solver::adjust_bound_for_int(lpvar j, lconstraint_kind& k, const mpq& bound) {
     if (!column_is_int(j))
         return bound;
     switch (k) {
-    case LT: 
+    case LT:
+        k = LE;
     case LE:
         return floor(bound);
-    case GT: 
+    case GT:
+        k = GE;
     case GE: 
         return ceil(bound);
-    case EQ:
+    case EQ:        
         return bound;
     default:
         UNREACHABLE();
@@ -2193,13 +2195,13 @@ bool lar_solver::tighten_term_bounds_by_delta(unsigned term_index, const impq& d
     }
     TRACE("cube", tout << "can tighten";);
     if (slv.column_has_upper_bound(j)) {
-        if (!is_zero(delta.y))
+        if (!is_zero(delta.y) || !is_zero(slv.m_upper_bounds[j].y))
             add_var_bound(tj, lconstraint_kind::LT, slv.m_upper_bounds[j].x - delta.x);
         else 
             add_var_bound(tj, lconstraint_kind::LE, slv.m_upper_bounds[j].x - delta.x);
     }
     if (slv.column_has_lower_bound(j)) {
-        if (!is_zero(delta.y))
+        if (!is_zero(delta.y) || !is_zero(slv.m_lower_bounds[j].y))
             add_var_bound(tj, lconstraint_kind::GT, slv.m_lower_bounds[j].x + delta.x);
         else 
             add_var_bound(tj, lconstraint_kind::GE, slv.m_lower_bounds[j].x + delta.x);
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 333ddd65b..fc45f8e7c 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -169,7 +169,7 @@ public:
 
     void add_new_var_to_core_fields_for_mpq(bool register_in_basis);
 
-    mpq adjust_bound_for_int(lpvar j, lconstraint_kind, const mpq&);
+    mpq adjust_bound_for_int(lpvar j, lconstraint_kind&, const mpq&);
 
 
     // terms
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index ce560b92b..728c3017f 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -504,6 +504,7 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::calc_current_x
     unsigned j = this->m_n();
     while (j--) {
         if (!column_is_feasible(j)) {
+            TRACE("lar_solver", tout << "infeasible column: "; print_column_info(j, tout) << "\n";);
             return false;
         }
     }