mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

port on Grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-09 16:41:03 -07:00
parent 3fd76b24af
commit 005021f74e
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/grobner/grobner.cpp
View file

@ -608,13 +608,12 @@ unsigned grobner::simplify_loop_on_target_monomials(equation const * source, equ
target->m_lc = false;
mul_append(1, source, coeff, rest, new_monomials);
del_monomial(curr);
target->m_monomials[i] = nullptr;
}
else {
target->m_monomials[n_sz++] = curr;
}
}
return n_sz < target->m_monomials.size();
return n_sz;
}
/**