diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 6aceaf669..b38eab508 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -282,7 +282,9 @@ public:
             return;
         TRACE("nla_cn", tout << "after split c=" << **c << "\nfront="; print_front(front, tout) << "\n";);
         if (front.empty()) {
+#ifdef Z3DEBUG
             TRACE("nla_cn", tout << "got the cn form: =" << *m_e <<  ", clone = " << *m_e_clone << "\n";);
+#endif
             m_done = m_call_on_result(m_e) || ++m_reported > 100;
 #ifdef Z3DEBUG
             SASSERT(nex_creator::equal(m_e, m_e_clone));
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 15cb0f6e7..2e4f1d911 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -25,7 +25,7 @@
 
 namespace nla {
 typedef intervals::interval interv;
-horner::horner(core * c) : common(c), m_intervals(c, c->reslim()), m_fixed_as_scalars(true) {}
+horner::horner(core * c) : common(c), m_intervals(c, c->reslim()), m_fixed_as_scalars(false) {}
 
 template <typename T>
 bool horner::row_has_monomial_to_refine(const T& row) const {
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 737a3de4a..b4311b186 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -500,7 +500,6 @@ nex * nex_creator::simplify_mul(nex_mul *e) {
 }
 
 nex* nex_creator::simplify_sum(nex_sum *e) {
-    TRACE("nla_cn", tout << lp::lp_settings::ddd << "\n";);
     TRACE("nla_cn_details", tout << "was e = " << *e << "\n";);
     simplify_children_of_sum(e->children());
     nex *r;