mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 18:15:32 +00:00
Code Activity

randomize m_to_refine() init

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-17 21:01:22 -07:00
parent 2560c9b739
commit faf39259b2
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.cpp
View file

@ -967,7 +967,7 @@ void core::init_to_refine() {
m_to_refine.clear();
unsigned r = random(), sz = m_emons.number_of_monomials();
for (unsigned k = 0; k < sz; k++) {
auto const & m = m_emons[(k + r)% sz];
auto const & m = *(m_emons.begin() + (k + r)% sz);
if (!check_monomial(m))
m_to_refine.push_back(m.var());
}