diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 64f6f5696..425013eb0 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -575,7 +575,7 @@ public:
     }
 
     std::ostream& print_column_info(unsigned j, std::ostream & out) const {
-        out << "j = " << j << ",\tname = "<< column_name(j) << "\t";
+        out << "[" << j << "],\tname = "<< column_name(j) << "\t";
         switch (m_column_types[j]) {
         case column_type::fixed:
         case column_type::boxed:
diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index b3270754c..4346c8b1c 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -57,7 +57,7 @@ void basics::generate_zero_lemmas(const monomial& m) {
     TRACE("nla_solver_details", tout << "zero_j = " << zero_j << ", sign = " << sign << "\n";);
     if (sign == 0) { // have to generate a non-convex lemma
         add_trival_zero_lemma(zero_j, m);
-    } else { 
+    } else { // here we know the sign of zero_j
         generate_strict_case_zero_lemma(m, zero_j, sign);
     }
     for (lpvar j : fixed_zeros)
@@ -88,7 +88,7 @@ void basics::get_non_strict_sign(lpvar j, int& sign) const {
 
 void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign) {
     if (product_sign == 0) {
-        TRACE("nla_solver_bl", tout << "zero product sign\n";);
+        TRACE("nla_solver_bl", tout << "zero product sign: " << pp_mon(_(), m)<< "\n"; );
         generate_zero_lemmas(m);
     } else {
         add_empty_lemma();
@@ -188,7 +188,7 @@ void basics::generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j,
     // we know all the signs
     add_empty_lemma();
     c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT));
-    for (unsigned j : m.rvars()){
+    for (unsigned j : m.vars()){
         if (j != zero_j) {
             negate_strict_sign(j);
         }
@@ -203,7 +203,7 @@ void basics::add_fixed_zero_lemma(const monomial& m, lpvar j) {
     TRACE("nla_solver", c().print_lemma(tout););
 }
 void basics::negate_strict_sign(lpvar j) {
-    TRACE("nla_solver_details", c().print_var(j, tout););
+    TRACE("nla_solver_details", tout << pp_var(c(), j) << "\n";);
     if (!vvr(j).is_zero()) {
         int sign = nla::rat_sign(vvr(j));
         c().mk_ineq(j, (sign == 1? llc::LE : llc::GE));
@@ -494,7 +494,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const fact
 }
 
 void basics::basic_lemma_for_mon_model_based(const monomial& rm) {
-    TRACE("nla_solver_bl", tout << "rm = " << rm;);
+    TRACE("nla_solver_bl", tout << "rm = " << pp_mon(_(), rm) << "\n";);
     if (vvr(rm).is_zero()) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
             if (factorization.is_empty())
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index fb4725dc8..829f09096 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -108,7 +108,7 @@ void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const
 
 void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d) {
     TRACE("nla_solver",  
-          tout << "ac=" << pp_mon(c(), ac) << "\nrm= " << bd << ", b= " << pp_fac(c(), b) << ", d= " << pp_var(c(), d) << "\n";);
+          tout << "ac=" << pp_mon(_(), ac) << "\nrm= " << pp_mon(_(), bd) << ", b= " << pp_fac(_(), b) << ", d= " << pp_var(_(), d) << "\n";);
     bool p = !k;
     lpvar a = ac.vars()[p];
     lpvar c = ac.vars()[k];