diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index c8ac58ad5..78ca6b726 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -973,7 +973,7 @@ namespace smt {
         /**
            \brief A monomial is 'pure' if does not have a numeric coefficient.
         */
-        bool is_pure_monomial(expr * m) const { return m_util.is_mul(m) && !m_util.is_numeral(to_app(m)->get_arg(0)); }
+        bool is_pure_monomial(expr * m) const { return m_util.is_mul(m) && (to_app(m)->get_num_args() > 2 || !m_util.is_numeral(to_app(m)->get_arg(0))); }
         bool is_pure_monomial(theory_var v) const { return is_pure_monomial(get_enode(v)->get_owner()); }
         void mark_var(theory_var v, svector<theory_var> & vars, var_set & already_found);
         void mark_dependents(theory_var v, svector<theory_var> & vars, var_set & already_found, row_set & already_visited_rows);
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index c538d78c4..23e11fb1e 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -349,7 +349,7 @@ namespace smt {
     */
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_mul_core(app * m) {
-        TRACE("internalize_mul_core", tout << "internalizing...\n" << mk_pp(m,get_manager()) << "\n";);
+        TRACE("internalize_mul_core", tout << "internalizing...\n" << mk_pp(m, get_manager()) << "\n";);
         if (!m_util.is_mul(m))
             return internalize_term_core(m);       
         for (expr* arg : *m) {
diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h
index 8e9ef878e..0277a5717 100644
--- a/src/smt/theory_arith_pp.h
+++ b/src/smt/theory_arith_pp.h
@@ -71,10 +71,8 @@ namespace smt {
         if (m_nl_monomials.empty())
             return;
         out << "non linear monomials:\n";
-        svector<theory_var>::const_iterator it  = m_nl_monomials.begin();
-        svector<theory_var>::const_iterator end = m_nl_monomials.end();
-        for (; it != end; ++it)
-            display_var(out, *it);
+        for (auto nl : m_nl_monomials) 
+            display_var(out, nl);
     }
 
     template<typename Ext>