diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index d146671ac..d51b9e159 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -165,10 +165,10 @@ interv horner::interval_of_mul(const nex& e) {
         interv c;
         m_intervals.mul(a, b, c, comb_rule);
         m_intervals.combine_deps(a, b, comb_rule, c);
-        TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a) << "\n";);
-        TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c) << "\n";);
+        TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a););
+        TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c););
         m_intervals.set(a, c);
-        TRACE("nla_horner_details", tout << "part mult "; m_intervals.display(tout, a) << "\n";);
+        TRACE("nla_horner_details", tout << "part mult "; m_intervals.display(tout, a););
     }
     TRACE("nla_horner_details",  tout << "e=" << e << "\n";
           tout << " return "; m_intervals.display(tout, a););
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 46ecda77f..f6bd9a5dc 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -275,14 +275,15 @@ std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& ou
 
 std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const {
     out << "expl: ";
+    unsigned i = 0;
     for (auto &p : exp) {
         out << "(" << p.second << ")";
         m_lar_solver.print_constraint_indices_only_customized(p.second,
                                                               [this](lpvar j) { return var_str(j);},
                                                               out);
-        out << "      ";
+        if (++i < exp.size())
+            out << "      ";
     }
-    out << "\n";
     return out;
 }
 
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 50c5d0f0a..9a59c016b 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -92,15 +92,23 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
     m_dep_manager.linearize(i.m_lower_dep, expl);
     {
         lp::explanation e(expl);
-        out << "\nlower constraints\n";
-        m_core->print_explanation(e, out);
-        expl.clear();
+        if (!expl.empty()) {
+            out << "\nlower constraints\n";
+            m_core->print_explanation(e, out);
+            expl.clear();
+        } else {
+            out << "\nno lower constraints\n";
+        }
     }
     m_dep_manager.linearize(i.m_upper_dep, expl);   
     {
         lp::explanation e(expl);
-        out << "upper constraints\n";    
-        m_core->print_explanation(e, out);
+        if (!expl.empty()) {
+            out << "upper constraints\n";    
+            m_core->print_explanation(e, out);
+        }else {
+            out << "no upper constraints\n";
+        }
     }
     return out;
 }