diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp
index 4b77fd6a9..b1dec694f 100644
--- a/src/util/lp/emonomials.cpp
+++ b/src/util/lp/emonomials.cpp
@@ -143,7 +143,7 @@ namespace nla {
             }
         }
         unsigned idx = m_monomials.size();
-        m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr(), idx));
+        m_monomials.push_back(monomial(v, vars, idx));
         m_var2index.setx(v, idx, UINT_MAX);
         do_canonize(m_monomials[idx]);
         monomial const* result = nullptr;
diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index bbc4c4e7f..58ed176d0 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -104,7 +104,7 @@ struct const_iterator_mon {
 };
 
 struct factorization_factory {
-    const svector<lpvar>& m_vars;
+    const svector<lpvar>  m_vars;
     const monomial*       m_monomial;
     // returns true if found
     virtual bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0;
diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index f6e6d9b66..393852d58 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -740,7 +740,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
     explain(f);
     TRACE("nla_solver",
           c().print_lemma(tout);
-          tout << "rm = " << rm;
+          tout << "rm = " << pp_rmon(c(), rm);
           );
     return true;
 }
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index a01e186d1..79451ed2b 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -173,8 +173,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
         print_var(f.var(), out);
     } 
     else {
-        out << " RM = " << m_emons[f.var()];
-        out << "\n orig mon = " << m_emons[f.var()];
+        out << " RM = " << pp_rmon(*this, m_emons[f.var()]);
     }
     return out;
 }
@@ -1447,8 +1446,8 @@ void core::trace_print_ol(const monomial& ac,
                           const monomial& bc,
                           const factor& b,
                           std::ostream& out) {
-    out << "ac = " << ac << "\n";
-    out << "bc = " << bc << "\n";
+    out << "ac = " << pp_mon(*this, ac) << "\n";
+    out << "bc = " << pp_mon(*this, bc) << "\n";
     out << "a = ";
     print_factor_with_vars(a, out);
     out << ", \nb = ";
@@ -1585,7 +1584,7 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*
             j = rm.var();
             sign = rm.rsign();
             TRACE("nla_solver", tout << "found bf";
-                  tout << ":rm:" << rm << "\n";
+                  tout << ":rm:" << pp_rmon(*this, rm) << "\n";
                   tout << "bf:"; print_bfc(bf, tout);
                   tout << ", product = " << val(rm) << ", but should be =" << val(bf.m_x)*val(bf.m_y);
                   tout << ", j == "; print_var(j, tout) << "\n";);
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index fc98db373..cfb77641d 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -187,8 +187,8 @@ bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
                                      bool k,
                                      const monomial& rm_bd) {
     TRACE("nla_solver", 
-          tout << "rm_ac = " << rm_ac << "\n";
-          tout << "rm_bd = " << rm_bd << "\n";
+          tout << "rm_ac = " << pp_rmon(_(), rm_ac) << "\n";
+          tout << "rm_bd = " << pp_rmon(_(), rm_bd) << "\n";
           tout << "ac_f[k] = ";
           c().print_factor_with_vars(ac_f[k], tout););
     factor b;