diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index c8e58cc14..b6f678fea 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2284,7 +2284,6 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) {
                    << " for function " << mk_pp(f,*this)
                    << " supplied sort is "
                    << mk_pp(actual_sort, *this);
-            SASSERT(false);
             throw ast_exception(buffer.str());
         }
     }
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index efca6c042..c7dc3462a 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -444,7 +444,7 @@ namespace smt {
         if (!gate_ctx) {
             mk_enode(n, true, true, false);
             set_enode_flag(v, true);
-            SASSERT(get_assignment(v) == l_undef);
+            SASSERT(get_assignment(v) == l_undef || get_assignment(l_def) != l_undef);
         }
     }
 
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index b009380f0..69786a66a 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1541,10 +1541,10 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
     rational a, b;
     unsigned n  = UINT_MAX;
     unsigned nm = UINT_MAX;
-    if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm)) {
+    if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm)) {        
         CTRACE("in_monovariate_monomials", n == nm,
                for (unsigned i = 0; i < p.size(); i++) {
-                                                        if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager());
+                   if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager());
                }
                tout << "\n";
                tout << "var: " << mk_pp(var, get_manager()) << "\n";
@@ -1554,6 +1554,7 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
                tout << "i2: "  << i2 << "\n";
                tout << "b: "   << b << "\n";
                tout << "nm: "  << nm << "\n";);
+        if (n == nm) return horner(p, var);
         SASSERT(n != nm);
         expr * new_expr = nullptr;
         if (nm < n) {