diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 4d948daf4..fa506b277 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -43,7 +43,9 @@ class create_cut {
     struct found_big {};
 
     const impq & get_value(unsigned j) const { return lia.get_value(j); }
-    bool is_real(unsigned j) const { return lia.is_real(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 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); }
@@ -53,7 +55,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(lia.column_is_int(j) && m_fj.is_pos());
+        lp_assert(is_int(j) && m_fj.is_pos());
         TRACE("gomory_cut_detail", 
               tout << " k = " << m_k;
               tout << ", fj: " << m_fj << ", ";
@@ -61,6 +63,7 @@ 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);
@@ -84,13 +87,15 @@ class create_cut {
     }
 
     void real_case_in_gomory_cut(const mpq & a, unsigned j) {
-        TRACE("gomory_cut_detail_real", tout << "real\n";);
+        TRACE("gomory_cut_detail_real", tout << "j = " << j << ", a = " << a << ", m_k = " << m_k << "\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
@@ -100,16 +105,20 @@ 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(); 
@@ -119,7 +128,6 @@ 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;
     }
 
@@ -131,19 +139,18 @@ 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(lia.column_is_int(v));
+            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);
-                // switch size
-                m_t.add_monomial(- mpq(1), v);
-                m_k.neg();
-            } else {
-                if (!m_k.is_int())
-                    m_k = floor(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);
             }
         } else {
             m_lcm_den = lcm(m_lcm_den, denominator(m_k));
@@ -153,14 +160,12 @@ class create_cut {
                 // normalize coefficients of integer parameters to be integers.
                 for (auto & pi: pol) {
                     pi.first *= m_lcm_den;
-                    SASSERT(!lia.column_is_int(pi.second) || pi.first.is_int());
+                    SASSERT(!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_k.neg();
+                m_t.add_monomial(pi.first, pi.second);
         }
         TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;);
         lp_assert(m_k.is_int());
@@ -207,7 +212,7 @@ class create_cut {
     }
 
     void dump_declaration(std::ostream& out, unsigned v) const {
-        out << "(declare-const " << var_name(v) << (lia.column_is_int(v) ? " Int" : " Real") << ")\n";
+        out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n";
     }
     
     void dump_declarations(std::ostream& out) const {
@@ -217,7 +222,7 @@ class create_cut {
         }
         for (const auto& p : m_t) {
             unsigned v = p.var();
-            if (tv::is_term(v)) {
+            if (lp::tv::is_term(v)) {
                 dump_declaration(out, v);
             }
         }
@@ -313,6 +318,11 @@ 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);
                 } 
@@ -334,8 +344,8 @@ public:
             return report_conflict_from_gomory_cut();
         if (some_int_columns)
             adjust_term_and_k_for_some_ints_case_gomory();
-        lp_assert(lia.current_solution_is_inf_on_cut());
         TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
+        lp_assert(lia.current_solution_is_inf_on_cut());
         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;
@@ -441,7 +451,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 = true;
+    lia.m_upper = false;
     return cut(lia.m_t, lia.m_k, lia.m_ex, j, row);
 }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index e3bd9c126..647a52990 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3481,10 +3481,7 @@ public:
 
     void dump_conflict() {
         if (dump_lemmas()) {
-            unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
-            (void)id;
-            std::cout << id << "\n";
-            SASSERT(id != 49);
+            ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
         }
     }