fix in gomory cut

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Mar 5, 2020 · e0411c1 · e0411c1
1 parent b16b16b
commit e0411c1
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
@@ -145,12 +145,13 @@ class create_cut {
             unsigned v = pol[0].second;
             lp_assert(is_int(v));
             const mpq& a = pol[0].first;
-            m_k /= a;
             if (a.is_pos()) { // we have av >= k
+                m_k /= a;
                 if (!m_k.is_int())
                     m_k = ceil(m_k);
                 m_t.add_monomial(mpq(1), v);
             } else {
+                m_k /= -a;
                 if (!m_k.is_int())
                     m_k = ceil(m_k);
                 m_t.add_monomial(-mpq(1), v);