From 9f8f6dee9ea75597306e77a167b4db7ebe5caa4c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 1 Oct 2019 10:41:45 -0700
Subject: [PATCH] fix mk_div

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h  |  3 ++-
 src/math/lp/nex_creator.cpp | 30 ++++++++++++++----------------
 2 files changed, 16 insertions(+), 17 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index f8fbe8dcf..f6fa24dcc 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -370,7 +370,8 @@ public:
             || (ce->is_var() && to_var(ce)->var() == j);
     }
     // all factors of j go to a, the rest to b
-    void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) {        
+    void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) {
+        TRACE("nla_cn_details", tout << "e = " << * e << ", j = " << m_nex_creator.ch(j) << std::endl;);
         a = m_nex_creator.mk_sum();
         m_b_split_vec.clear();
         for (nex * ce: e->children()) {
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 15756b0cb..e2fbcbbff 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -20,9 +20,9 @@
 #include "math/lp/nex_creator.h"
 #include <map>
 namespace nla {
+
 nex * nex_creator::mk_div(const nex* a, lpvar j) {
     SASSERT(is_simplified(a));
-    TRACE("nla_cn_details", tout << "a=" << *a << ", " << ch(j) << "\n";);
     SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j));
     if (a->is_var())
         return mk_scalar(rational(1));
@@ -31,23 +31,21 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
     for (auto& p : to_mul(a)->children()) {
         const nex * c = p.e();
         int pow = p.pow();
-        if (!seenj) {
-            if (c->contains(j)) {
-                if (!c->is_var()) {                    
-                    bv.push_back(nex_pow(mk_div(c, j)));
-                    if (pow != 1) {
-                        bv.push_back(nex_pow(clone(c), pow)); 
-                    }
-                } else {
-                    SASSERT(to_var(c)->var() == j);
-                    if (p.pow() != 1) {
-                        bv.push_back(nex_pow(mk_var(j), pow - 1));
-                    }
+        if (!seenj && c->contains(j)) {
+            if (!c->is_var()) {                    
+                bv.push_back(nex_pow(mk_div(c, j)));
+                if (pow != 1) {
+                    bv.push_back(nex_pow(clone(c), pow - 1)); 
                 }
-                seenj = true;
-            } 
+            } else {
+                SASSERT(to_var(c)->var() == j);
+                if (p.pow() != 1) {
+                    bv.push_back(nex_pow(mk_var(j), pow - 1));
+                }
+            }
+            seenj = true;
         } else {
-            bv.push_back(nex_pow(clone(c)));
+            bv.push_back(nex_pow(clone(c), pow));
         }
     }
     if (bv.size() > 1) {