From 8c122ba9bd6840d08453b33a3ec5f9c388c3883f Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Sat, 15 Sep 2018 17:33:35 -0700
Subject: [PATCH] fixes in gomory cut

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp |  3 +--
 src/util/lp/gomory.cpp | 22 +++++++---------------
 2 files changed, 8 insertions(+), 17 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d976df56a..f8e2f9fe1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1704,11 +1704,10 @@ public:
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
-        /*
         if (!check_idiv_bounds()) {
             TRACE("arith", tout << "idiv bounds check\n";);
             return l_false;
-            }*/
+        }
         lp::lar_term term;
         lp::mpq k;
         lp::explanation ex; // TBD, this should be streamlined accross different explanations
diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp
index ec6877536..244244da0 100644
--- a/src/util/lp/gomory.cpp
+++ b/src/util/lp/gomory.cpp
@@ -55,26 +55,18 @@ class gomory::imp {
         mpq new_a;
         mpq one_minus_fj = 1 - fj;
         if (at_lower(j)) {
-            bool go_for_pos_a = fj / one_minus_f0 <  one_minus_fj / f0;
-            if (go_for_pos_a) {
-                new_a = fj / one_minus_f0;
-            }
-            else {
-                new_a = one_minus_fj / f0;
-            }
+            mpq fj_over_one_min_f0 = fj / one_minus_f0;
+            mpq one_minus_fj_over_f0 = one_minus_fj / f0;
+            new_a = fj_over_one_min_f0 < one_minus_fj_over_f0? fj_over_one_min_f0 : one_minus_fj_over_f0;
             m_k.addmul(new_a, lower_bound(j).x);
             m_ex.push_justification(column_lower_bound_constraint(j), new_a);
         }
         else {
-            bool go_for_pos_a = fj / f0 < one_minus_fj / one_minus_f0;
+            mpq fj_over_f0 = fj / f0;
+            mpq one_minus_fj_over_one_minus_f0 = one_minus_fj / one_minus_f0;
             lp_assert(at_upper(j));
-            // the upper terms are inverted
-            if (go_for_pos_a) {
-                new_a = - fj / f0;
-            }
-            else {
-                new_a =  - one_minus_fj / one_minus_f0;
-            }
+            // the upper terms are inverted - therefore we have -
+            new_a = - (fj_over_f0 < one_minus_fj_over_one_minus_f0? fj_over_f0 : one_minus_fj_over_one_minus_f0);
             m_k.addmul(new_a, upper_bound(j).x);
             m_ex.push_justification(column_upper_bound_constraint(j), new_a);
         }