mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix the nla_exp division

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-25 12:34:12 -07:00
parent d4a88f1de6
commit 5248a2dcab
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/nla_expr.h
View file

@ -334,9 +334,12 @@ public:
k--; k--;
} }
} }
SASSERT(powers.size() == 0);
while(k ++ < i) while(k ++ < i)
children().pop_back(); children().pop_back();
if (children().size() == 0)
*this = scalar(T(1));
return *this; return *this;
} }