diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index a6eea6021..9de63a6fc 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -336,6 +336,7 @@ lia_move int_solver::proceed_with_gomory_cut(lar_term& t, mpq& k, explanation& e
 lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
     if (m_iter_on_gomory_row != nullptr) {
         auto ret = proceed_with_gomory_cut(t, k, ex);
+        TRACE("gomory_cut", tout << "term t = "; m_lar_solver->print_term_as_indices(t, tout););
         if (ret != lia_move::continue_with_check)
             return ret;
     }
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 96313703a..2e8631445 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1192,6 +1192,13 @@ void lar_solver::print_term(lar_term const& term, std::ostream & out) const {
     print_linear_combination_of_column_indices(term.coeffs_as_vector(), out);
 }
 
+void lar_solver::print_term_as_indices(lar_term const& term, std::ostream & out) const {
+    if (!numeric_traits<mpq>::is_zero(term.m_v)) {
+        out << term.m_v << " + ";
+    }
+    print_linear_combination_of_column_indices_only(term.coeffs_as_vector(), out);
+}
+
 mpq lar_solver::get_left_side_val(const lar_base_constraint &  cns, const std::unordered_map<var_index, mpq> & var_map) const {
     mpq ret = cns.get_free_coeff_of_left_side();
     for (auto & it : cns.get_left_side_coefficients()) {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 9afb4180b..46af1ae63 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -381,12 +381,14 @@ public:
 
     void print_constraints(std::ostream& out) const ;
 
-    void print_terms(std::ostream& out) const ;
+    void print_terms(std::ostream& out) const;
 
     void print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const;
 
     void print_term(lar_term const& term, std::ostream & out) const;
 
+    void print_term_as_indices(lar_term const& term, std::ostream & out) const;
+
     mpq get_left_side_val(const lar_base_constraint &  cns, const std::unordered_map<var_index, mpq> & var_map) const;
 
     void print_constraint(const lar_base_constraint * c, std::ostream & out) const;