From a7123062a0bd8802fc5a07207a9e3fefd03b510c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 10 Apr 2020 11:21:30 -0700
Subject: [PATCH] fix #3899 regression from transitioning to decompose_monomial

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_parallel.cpp  |  2 +-
 src/smt/theory_arith_nl.h | 23 +++++++++++++----------
 2 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 31acd8872..14f064fa5 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -183,7 +183,7 @@ namespace smt {
             }
         };
 
-        num_threads = 1;
+        // num_threads = 1;
 
         while (true) {
             vector<std::thread> threads(num_threads);
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index d77a3de9c..6de40d87e 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1339,20 +1339,23 @@ expr * theory_arith<Ext>::factor(expr * m, expr * var, unsigned d) {
         m_nl_new_exprs.push_back(result);
         return result;
     }
-    SASSERT(is_pure_monomial(m));
-    unsigned idx = 0;
+
     ptr_buffer<expr> new_args;
-    for (expr * arg : *to_app(m)) {
-        if (arg == var) {
-            if (idx < d)
-                idx++;
-            else
-                new_args.push_back(arg);
-        }
-        else {
+    unsigned idx = 0;
+    auto insert = [&](expr* arg) {
+        if (idx < d && var == arg)
+            ++idx;
+        else
             new_args.push_back(arg);
+    };
+    while (m_util.is_mul(m) && idx < d) {
+        unsigned sz = to_app(m)->get_num_args();
+        for (unsigned i = 0; i + 1 < sz; ++i) {
+            insert(to_app(m)->get_arg(i));
         }
+        m = to_app(m)->get_arg(sz - 1);
     }
+    insert(m);
     SASSERT(idx == d);
     TRACE("factor_bug", tout << "new_args:\n"; for(unsigned i = 0; i < new_args.size(); i++) tout << mk_pp(new_args[i], get_manager()) << "\n";);
     expr * result = mk_nary_mul(new_args.size(), new_args.c_ptr(), m_util.is_int(var));