From 0c6336c85dc672bf11f47a866646e365743cf2d0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 2 Oct 2019 12:00:14 -0700 Subject: [PATCH] fix nex simplification Signed-off-by: Lev Nachmanson --- src/math/lp/nex_creator.cpp | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index 961c3dcee..148a15ea9 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -410,19 +410,20 @@ bool nex_creator::register_in_join_map(std::map& map, ne void nex_creator::process_mul_in_simplify_sum(nex_mul* em, std::map &map, vector & tmp) { auto it = em->children().begin(); if (it->e()->is_scalar()) { + SASSERT(it->pow() == 1); rational r = to_scalar(it->e())->value(); auto end = em->children().end(); if (em->children().size() == 2 && em->children()[1].pow() == 1) { register_in_join_map(map, em->children()[1].e(), r); - } - SASSERT(it->pow() == 1); - tmp.push_back(nex_mul()); - nex_mul * m = &tmp[tmp.size()-1]; - for (it++; it != end; it++) { - m->add_child_in_power(it->e(), it->pow()); - } - if (!register_in_join_map(map, m, r)) - tmp.pop_back(); + } else { + tmp.push_back(nex_mul()); + nex_mul * m = &tmp[tmp.size()-1]; + for (it++; it != end; it++) { + m->add_child_in_power(it->e(), it->pow()); + } + if (!register_in_join_map(map, m, r)) + tmp.pop_back(); + } } else { register_in_join_map(map, em, rational(1)); }