diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index fd2dc0da2..f096d1dd5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1629,6 +1629,7 @@ public:
     expr_ref term2expr(lp::lar_term const& term) {
         expr_ref t(m);
         expr_ref_vector ts(m);
+        ts.push_back(a.mk_numeral(term.m_v, true));
         for (auto const& p : term) {
             lp::var_index wi = p.var();
             if (m_solver->is_term(wi)) {
diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp
index 55098dccf..9974eda7f 100644
--- a/src/util/lp/gomory.cpp
+++ b/src/util/lp/gomory.cpp
@@ -168,11 +168,13 @@ public:
         mpq one_min_f0 = 1 - f0;
         for (const auto & p : m_row) {
             unsigned j = p.var();
+#if 1
             if (column_is_fixed(j)) {
                 m_ex.push_justification(column_lower_bound_constraint(j));
                 m_ex.push_justification(column_upper_bound_constraint(j));
                 continue;
             }
+#endif
             if (j == m_inf_col) {
                 lp_assert(p.coeff() == one_of_type<mpq>());
                 TRACE("gomory_cut_detail", tout << "seeing basic var";);
@@ -194,7 +196,7 @@ public:
             adjust_term_and_k_for_some_ints_case_gomory(lcm_den);
         lp_assert(m_int_solver.current_solution_is_inf_on_cut());
         m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k);
-        TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout); tout << " <= " << m_k << std::endl;);
+        TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout) << " <= " << m_k << std::endl;);
         return lia_move::cut;
     }
     imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) :
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 41b6fe31d..9a6549917 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -577,7 +577,7 @@ public:
     }
 
     void print_column_info(unsigned j, std::ostream & out) const {
-        out << "j = " << j << ", name = "<< column_name(j);
+        out << "j = " << j << ",\tname = "<< column_name(j) << "\t";
         switch (m_column_types[j]) {
         case column_type::fixed:
         case column_type::boxed:
@@ -596,11 +596,11 @@ public:
             lp_assert(false);
         }
         //        out << "basis heading = " << m_basis_heading[j] << std::endl;
-        out << " x =                " << m_x[j];
+        out << "\tx = " << m_x[j];
         if (m_basis_heading[j] >= 0)
             out << " base\n";
         else
-            out << " nbas\n";
+           out << " \n";
     }
 
     bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; }