diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index fa506b277..4d948daf4 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -43,9 +43,7 @@ class create_cut {
     struct found_big {};
 
     const impq & get_value(unsigned j) const { return lia.get_value(j); }
-    bool is_int(unsigned j) const { return lia.column_is_int(j) || (lia.is_fixed(j) &&
-                                                             lia.lra.column_lower_bound(j).is_int()); }
-    bool is_real(unsigned j) const { return !is_int(j); }
+    bool is_real(unsigned j) const { return lia.is_real(j); }
     bool at_lower(unsigned j) const { return lia.at_lower(j); }
     bool at_upper(unsigned j) const { return lia.at_upper(j); }
     const impq & lower_bound(unsigned j) const { return lia.lower_bound(j); }
@@ -55,7 +53,7 @@ class create_cut {
     bool column_is_fixed(unsigned j) const { return lia.lra.column_is_fixed(j); }
 
     void int_case_in_gomory_cut(unsigned j) {
-        lp_assert(is_int(j) && m_fj.is_pos());
+        lp_assert(lia.column_is_int(j) && m_fj.is_pos());
         TRACE("gomory_cut_detail", 
               tout << " k = " << m_k;
               tout << ", fj: " << m_fj << ", ";
@@ -63,7 +61,6 @@ class create_cut {
               );
         mpq new_a;
         if (at_lower(j)) {
-            // here we have the product of new_a*(xj - lb(j)), so new_a*lb(j) is added to m_k
             new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f);
             lp_assert(new_a.is_pos());
             m_k.addmul(new_a, lower_bound(j).x);
@@ -87,15 +84,13 @@ class create_cut {
     }
 
     void real_case_in_gomory_cut(const mpq & a, unsigned j) {
-        TRACE("gomory_cut_detail_real", tout << "j = " << j << ", a = " << a << ", m_k = " << m_k << "\n";);
+        TRACE("gomory_cut_detail_real", tout << "real\n";);
         mpq new_a;
         if (at_lower(j)) {
             if (a.is_pos()) {
-                // the delta is a (x - f) is positive it has to grow and fight m_one_minus_f
                 new_a = a / m_one_minus_f;
             }
             else {
-                // the delta is negative and it works again m_f
                 new_a = - a / m_f;
             }
             m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than
@@ -105,20 +100,16 @@ class create_cut {
         else {
             lp_assert(at_upper(j));
             if (a.is_pos()) {
-                // the delta is works again m_f
                 new_a =  - a / m_f; 
             }
             else {
-                // the delta is positive works again m_one_minus_f
                 new_a =   a / m_one_minus_f; 
             }
             m_k.addmul(new_a, upper_bound(j).x); //  k += upper_bound(j).x * new_a; 
             m_ex->push_justification(column_upper_bound_constraint(j));
         }
+        TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";);
         m_t.add_monomial(new_a, j);
-        TRACE("gomory_cut_detail_real", tout << "add " << new_a << "*v" << j << ", k: " << m_k << "\n";
-              tout << "m_t =  "; lia.lra.print_term(m_t, tout) << "\nk: " << m_k << "\n";);
-        
 #if SMALL_CUTS
         // if (numerator(new_a).is_big()) throw found_big(); 
         if (numerator(new_a) > m_big_number) throw found_big(); 
@@ -128,6 +119,7 @@ class create_cut {
     lia_move report_conflict_from_gomory_cut() {
         lp_assert(m_k.is_pos());
         // conflict 0 >= k where k is positive
+        m_k.neg(); // returning 0 <= -k
         return lia_move::conflict;
     }
 
@@ -139,18 +131,19 @@ class create_cut {
         if (pol.size() == 1) {
             TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;);
             unsigned v = pol[0].second;
-            lp_assert(is_int(v));
+            lp_assert(lia.column_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);
+                // switch size
+                m_t.add_monomial(- mpq(1), v);
+                m_k.neg();
             } else {
-                m_k /= -a;
                 if (!m_k.is_int())
-                    m_k = ceil(m_k);
-                m_t.add_monomial(-mpq(1), v);
+                    m_k = floor(m_k);
+                m_t.add_monomial(mpq(1), v);
             }
         } else {
             m_lcm_den = lcm(m_lcm_den, denominator(m_k));
@@ -160,12 +153,14 @@ class create_cut {
                 // normalize coefficients of integer parameters to be integers.
                 for (auto & pi: pol) {
                     pi.first *= m_lcm_den;
-                    SASSERT(!is_int(pi.second) || pi.first.is_int());
+                    SASSERT(!lia.column_is_int(pi.second) || pi.first.is_int());
                 }
                 m_k *= m_lcm_den;
             }
+            // negate everything to return -pol <= -m_k
             for (const auto & pi: pol)
-                m_t.add_monomial(pi.first, pi.second);
+                m_t.add_monomial(-pi.first, pi.second);
+            m_k.neg();
         }
         TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;);
         lp_assert(m_k.is_int());
@@ -212,7 +207,7 @@ class create_cut {
     }
 
     void dump_declaration(std::ostream& out, unsigned v) const {
-        out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n";
+        out << "(declare-const " << var_name(v) << (lia.column_is_int(v) ? " Int" : " Real") << ")\n";
     }
     
     void dump_declarations(std::ostream& out) const {
@@ -222,7 +217,7 @@ class create_cut {
         }
         for (const auto& p : m_t) {
             unsigned v = p.var();
-            if (lp::tv::is_term(v)) {
+            if (tv::is_term(v)) {
                 dump_declaration(out, v);
             }
         }
@@ -318,11 +313,6 @@ public:
 
              // use -p.coeff() to make the format compatible with the format used in: Integrating Simplex with DPLL(T)
             try {
-                if (lia.is_fixed(j)) {
-                    m_ex->push_justification(column_lower_bound_constraint(j));
-                    m_ex->push_justification(column_upper_bound_constraint(j));
-                    continue;
-                }
                 if (is_real(j)) {  
                     real_case_in_gomory_cut(- p.coeff(), j);
                 } 
@@ -344,8 +334,8 @@ public:
             return report_conflict_from_gomory_cut();
         if (some_int_columns)
             adjust_term_and_k_for_some_ints_case_gomory();
-        TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
         lp_assert(lia.current_solution_is_inf_on_cut());
+        TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
         lia.lra.subs_term_columns(m_t);
         TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
         return lia_move::cut;
@@ -451,7 +441,7 @@ lia_move gomory::operator()() {
     const row_strip<mpq>& row = lra.get_row(r);
     SASSERT(lra.row_is_correct(r));
     SASSERT(is_gomory_cut_target(row));
-    lia.m_upper = false;
+    lia.m_upper = true;
     return cut(lia.m_t, lia.m_k, lia.m_ex, j, row);
 }