diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 7c7320a73..ae45198ce 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1365,6 +1365,16 @@ std::ostream& lar_solver::print_constraint(constraint_index ci, std::ostream & o
     return print_constraint(m_constraints[ci], out);
 }
 
+std::ostream& lar_solver::print_constraint_indices_only(constraint_index ci, std::ostream & out) const {
+    if (ci >= m_constraints.size()) {
+        out << "constraint " << T_to_string(ci) << " is not found";
+        out << std::endl;
+        return out;
+    }
+
+    return print_constraint_indices_only(m_constraints[ci], out);
+}
+
 std::ostream& lar_solver::print_constraints(std::ostream& out) const  {
     out << "number of constraints = " << m_constraints.size() << std::endl;
     for (auto c : m_constraints) {
@@ -1388,6 +1398,14 @@ std::ostream& lar_solver::print_left_side_of_constraint(const lar_base_constrain
     return out;
 }
 
+std::ostream& lar_solver::print_left_side_of_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const {
+    print_linear_combination_of_column_indices_only(c->coeffs(), out);
+    mpq free_coeff = c->get_free_coeff_of_left_side();
+    if (!is_zero(free_coeff))
+        out << " + " << free_coeff;
+    return out;
+}
+
 std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) const {
     if (term.size() == 0){
         out << "0";
@@ -1434,6 +1452,11 @@ std::ostream& lar_solver::print_constraint(const lar_base_constraint * c, std::o
     return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl;
 }
 
+std::ostream& lar_solver::print_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const {
+    print_left_side_of_constraint_indices_only(c, out);
+    return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl;
+}
+
 void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector<unsigned>& column_list) {
     for (unsigned i = 0; i < sz; i++) {        
         var_index var = vars[i];
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 35f138f80..8e117b67a 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -503,15 +503,20 @@ public:
 
     std::ostream& print_constraints(std::ostream& out) const ;
 
+    std::ostream& print_constraint_indices_only(constraint_index ci, std::ostream & out) const;
+
     std::ostream& print_terms(std::ostream& out) const;
 
     std::ostream& print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const;
 
+    std::ostream& print_left_side_of_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const;
+
     std::ostream& print_term(lar_term const& term, std::ostream & out) const;
 
     std::ostream& print_term_as_indices(lar_term const& term, std::ostream & out) const;
 
     std::ostream& print_constraint(const lar_base_constraint * c, std::ostream & out) const;
+    std::ostream& print_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const;
 
     std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const;
 
diff --git a/src/util/lp/lp_solver_def.h b/src/util/lp/lp_solver_def.h
index 8cd0f620e..e84535170 100644
--- a/src/util/lp/lp_solver_def.h
+++ b/src/util/lp/lp_solver_def.h
@@ -29,6 +29,8 @@ template <typename T, typename X> column_info<T> * lp_solver<T, X>::get_or_creat
 
 template <typename T, typename X>
 std::string lp_solver<T, X>::get_variable_name(unsigned j) const { // j here is the core solver index
+    if (!m_settings.m_print_external_var_name)
+        return std::string("v")+T_to_string(j);
     auto it = this->m_core_solver_columns_to_external_columns.find(j);
     if (it == this->m_core_solver_columns_to_external_columns.end())
         return std::string("x")+T_to_string(j);
diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h
index 6dc513afe..573c93abd 100644
--- a/src/util/lp/lp_utils.h
+++ b/src/util/lp/lp_utils.h
@@ -98,7 +98,30 @@ void print_linear_combination_of_column_indices_only(const T & coeffs, std::ostr
         else 
             out << T_to_string(val);
         
-        out << "x" << it.var();
+        out << "v" << it.var();
+    }
+}
+template <typename T>
+void print_linear_combination_of_column_indices_only(const vector<std::pair<T, unsigned>> & coeffs, std::ostream & out) {
+    bool first = true;
+    for (const auto & it : coeffs) {
+        auto val = it.first;
+        if (first) {
+            first = false;
+        } else {
+            if (val.is_pos()) {
+                out << " + ";
+            } else {
+                out << " - ";
+                val = -val;
+            }
+        }
+        if (val == 1)
+            out << " ";
+        else 
+            out << T_to_string(val);
+        
+        out << "v" << it.second;
     }
 }
 
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index 08a120c17..e7365072c 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -262,7 +262,7 @@ std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream&
     out << "expl: ";
     for (auto &p : exp) {
         out << "(" << p.second << ")";
-        m_lar_solver.print_constraint(p.second, out);
+        m_lar_solver.print_constraint_indices_only(p.second, out);
         out << "      ";
     }
     out << "\n";
@@ -403,13 +403,13 @@ bool core:: explain_by_equiv(const lp::lar_term& t, lp::explanation& e) {
         return false;
             
     m_evars.explain(signed_var(i, false), signed_var(j, sign), e);
-    TRACE("nla_solver", tout << "explained :"; m_lar_solver.print_term(t, tout););
+    TRACE("nla_solver", tout << "explained :"; m_lar_solver.print_term_as_indices(t, tout););
     return true;
             
 }
     
 void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) {
-    TRACE("nla_solver_details", m_lar_solver.print_term(t, tout << "t = "););
+    TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = "););
     if (!explain_ineq(t, cmp, rs)) {
         m_lar_solver.subs_term_columns(t);
         current_lemma().push_back(ineq(cmp, t, rs));
@@ -747,7 +747,7 @@ bool core:: var_is_fixed(lpvar j) const {
 }
     
 std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
-    m_lar_solver.print_term(in.m_term, out);
+    m_lar_solver.print_term_as_indices(in.m_term, out);
     out << " " << lconstraint_kind_string(in.m_cmp) << " " << in.m_rs;
     return out;
 }
@@ -1229,7 +1229,7 @@ void core::collect_equivs() {
             continue;
         lpvar j = s.external_to_local(ti);
         if (var_is_fixed_to_zero(j)) {
-            TRACE("nla_solver_eq", tout << "term = "; s.print_term(*s.terms()[i], tout););
+            TRACE("nla_solver_eq", tout << "term = "; s.print_term_as_indices(*s.terms()[i], tout););
             add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j));
         }
     }
diff --git a/src/util/lp/nla_monotone_lemmas.cpp b/src/util/lp/nla_monotone_lemmas.cpp
index d1d2bf031..564a35933 100644
--- a/src/util/lp/nla_monotone_lemmas.cpp
+++ b/src/util/lp/nla_monotone_lemmas.cpp
@@ -91,6 +91,7 @@ void monotone::monotonicity_lemma(monomial const& m) {
 }
 
 void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val) {
+    TRACE("nla_solver", tout << "prod_val = " << prod_val << "\n";);
     add_empty_lemma();
     for (lpvar j : m.vars()) {
         c().add_abs_bound(j, llc::GT);