mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix a bug in gt_on_powers_mul_same_degree()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-08 10:06:39 -08:00
parent 35efc91aff
commit ec1b14a2f0
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/nex_creator.cpp
View file

@ -109,7 +109,6 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
template <typename T>
bool nex_creator::gt_on_powers_mul_same_degree(const T& a, const nex_mul& b) const {
bool ret = false;
std::cout << "'";
unsigned a_pow = a.begin()->pow();
unsigned b_pow = b.begin()->pow();
for (auto it_a = a.begin(), it_b = b.begin(); it_a != a.end() && it_b != b.end(); ) {