diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index 05640f0cf..477ea8094 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -37,7 +37,7 @@ void order::order_lemma() {
 
 void order::order_lemma_on_rmonomial(const smon& rm) {
     TRACE("nla_solver_details",
-          tout << "rm = " << rm << ", orig = " << c().m_emons[rm];);
+          tout << "rm = " << rm << ", orig = " << pp_mon(c(), c().m_emons[rm]););
 
     for (auto ac : factorization_factory_imp(rm, c())) {
         if (ac.size() != 2)