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

integrating NB suggestions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-11 09:28:12 -10:00
parent 40c81d14d8
commit bc302285a1
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -89,8 +89,8 @@ bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational& coeff) { void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational& coeff) {
TRACE("grobner_d", print_vector(children, tout);); TRACE("grobner_d", print_vector(children, tout););
vector<nex_pow> to_promote; vector<nex_pow> to_promote;
int skipped = 0; bool skipped = false;
for (unsigned j = 0; j < children.size(); j++) { for (nex_pow& p : children.size()) {
nex_pow& p = children[j]; nex_pow& p = children[j];
if (eat_scalar_pow(coeff, p, 1)) { if (eat_scalar_pow(coeff, p, 1)) {
skipped++; skipped++;
@ -654,8 +654,9 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
continue; continue;
} }
else { else {
if (skipped) if (skipped)
children[j++] = e; children[j] = e;
j++;
} }
} }
children.shrink(j); children.shrink(j);