From 5248a2dcabaa4f2899222fb131a4a37c3ae7b48b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 25 Jul 2019 12:34:12 -0700
Subject: [PATCH] fix the nla_exp division
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/nla_expr.h | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index e9717f4d6..0e7d287c0 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -334,9 +334,12 @@ public:
k--;
}
}
-
+ SASSERT(powers.size() == 0);
while(k ++ < i)
children().pop_back();
+
+ if (children().size() == 0)
+ *this = scalar(T(1));
return *this;
}