diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index f951af5de..2c11cc558 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -206,7 +206,11 @@ interv horner::interval_of_mul(const nex& e) {
 
 void horner::add_mul_to_vector(const nex& e, vector<std::pair<rational, lpvar>> &v) {
     TRACE("nla_horner_details", tout << e << "\n";);
-    SASSERT(e.is_mul() && e.children().size() == 2);
+    SASSERT(e.is_mul() && e.size() > 0);
+    if (e.size() == 1) {
+        add_linear_to_vector(*(e.children().begin()), v);
+        return;
+    }
     rational r;
     lpvar j = -1;
     for (const nex & c : e.children()) {
@@ -236,9 +240,8 @@ void horner::add_linear_to_vector(const nex& e, vector<std::pair<rational, lpvar
         v.push_back(std::make_pair(rational(1), e.var()));
         break;
     default:
-        TRACE("nla_horner_details", tout << e.type() << "\n";);
-        UNREACHABLE();
-        SASSERT(false);
+        SASSERT(!e.is_sum());
+        // noop
     }
 }
 // e = a * can_t + b
@@ -253,7 +256,9 @@ lp::lar_term horner::expression_to_normalized_term(nex& e, rational& a, rational
             b += c.value();
         } else {
             add_linear_to_vector(c, v);
-            if (v.size() == 1 || smallest_j > v.back().second) {
+            if (v.empty())
+                continue;
+            if (v.size() == 1 ||  smallest_j > v.back().second) {
                 smallest_j = v.back().second;
                 a_index = v.size() - 1;
             }
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index f1e00d266..83be7f5eb 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -177,7 +177,7 @@ public:
         }
     }
 
-    unsigned size() {
+    unsigned size() const {
         switch(m_type) {
         case expr_type::SUM:
         case expr_type::MUL:
@@ -376,20 +376,20 @@ public:
         return *this;
     }
 
+    // we need a linear combination of at least two variables
     bool sum_is_a_linear_term() const {
         SASSERT(is_sum());
-        int degree = 0;
+        TRACE("nla_expr_details", tout << *this << "\n";);
         unsigned number_of_non_scalars = 0;
         for (auto & e : children()) {
             int d = e.get_degree();
-            if (d > 1)
-                return false;
-            if (d > degree)
-                degree = d;
-            if (!e.is_scalar())
-                number_of_non_scalars++;
+            if (d == 0) continue;
+            if (d > 1) return false;
+            
+            number_of_non_scalars++;
         }
-        return degree == 1 && number_of_non_scalars > 1;
+        TRACE("nla_expr_details", tout << (number_of_non_scalars > 1?"linear":"non-linear") << "\n";); 
+        return number_of_non_scalars > 1;
     }
 
     int get_degree() const {