From 292e72ce0cee2caa5bab45ccdbb0a4817b308d2d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Sep 2019 08:36:10 -0700
Subject: [PATCH] fix #2590

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/arith_rewriter.cpp  |  2 +-
 src/ast/rewriter/poly_rewriter_def.h | 14 +++++++++++++-
 src/smt/theory_arith_nl.h            |  9 ++++-----
 3 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index c9df5bb37..174553a9b 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -86,7 +86,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     case OP_TANH: SASSERT(num_args == 1); st = mk_tanh_core(args[0], result); break;
     default: st = BR_FAILED; break;
     }
-    CTRACE("arith_rewriter", st != BR_FAILED, tout << mk_pp(f, m());
+    CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m());
             for (unsigned i = 0; i < num_args; ++i) tout << mk_pp(args[i], m()) << " ";
             tout << "\n==>\n" << mk_pp(result.get(), m()) << "\n";);
     return st;
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 5cf4cd449..1de0ce5fc 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -289,6 +289,18 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
         }
     }
 
+    if (num_coeffs > 1 || (num_coeffs == 1 && !is_numeral(args[0]))) {
+        ptr_buffer<expr> m_args;
+        for (unsigned i = 0; i < num_args; i ++) {
+            if (!is_numeral(args[i])) {
+                m_args.push_back(args[i]);
+            }
+        }
+        result = mk_mul_app(c, mk_mul_app(m_args.size(), m_args.c_ptr()));
+        return BR_REWRITE2;
+    }
+
+
     SASSERT(num_coeffs <= num_args - 2);
 
     if (!m_som || num_add == 0) {
@@ -363,7 +375,7 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
         for (unsigned i = 0; i < num_args; i++) {
             expr * const * v = sums[i];
             expr * arg       = v[it[i]];
-            m_args.push_back(arg);
+            m_args.push_back(arg);            
         }
         sum.push_back(mk_mul_app(m_args.size(), m_args.c_ptr()));
     }
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 78c3e2a39..b828b213a 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1217,10 +1217,8 @@ namespace smt {
             m_var2num_occs.insert(VAR, occs);                                                           \
         }
 
-        typename sbuffer<coeff_expr>::const_iterator it  = p.begin();
-        typename sbuffer<coeff_expr>::const_iterator end = p.end();
-        for (; it != end; ++it) {
-            expr * m = it->second;
+        for (coeff_expr const& kv : p) {
+            expr * m = kv.second;
             if (is_pure_monomial(m)) {
                 unsigned num_vars = get_num_vars_in_monomial(m);
                 for (unsigned i = 0; i < num_vars; i++) {
@@ -1237,6 +1235,7 @@ namespace smt {
             else {
                 TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
                 UNREACHABLE();
+                return;
             }
         }
 
@@ -1253,7 +1252,6 @@ namespace smt {
     template<typename Ext>
     expr * theory_arith<Ext>::p2expr(sbuffer<coeff_expr> & p) {
         SASSERT(!p.empty());
-        TRACE("p2expr_bug", display_coeff_exprs(tout, p););
         ptr_buffer<expr> args;
         for (coeff_expr const& ce : p) {
             rational const & c = ce.first;
@@ -1275,6 +1273,7 @@ namespace smt {
         SASSERT(!args.empty());
         expr * r = mk_nary_add(args.size(), args.c_ptr());
         m_nl_new_exprs.push_back(r);
+        TRACE("p2expr_bug", display_coeff_exprs(tout, p); tout << mk_pp(r, get_manager()) << "\n";);
         return r;
     }