mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 18:36:16 +00:00
Code Activity

better model based lemmaas

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-03-06 15:11:13 +14:00
parent 8dec4bf8d0
commit d1a5635b4a
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/util/lp/nla_solver.cpp
View file

@ -958,13 +958,14 @@ struct solver::imp {
int product_sign = rat_sign(m); int product_sign = rat_sign(m);
if (mon_sign != product_sign) { if (mon_sign != product_sign) {
basic_sign_lemma_model_based_one_mon(m, product_sign); basic_sign_lemma_model_based_one_mon(m, product_sign);
return true; if (done())
return true;
} }
i++; i++;
if (i == m_to_refine.size()) if (i == m_to_refine.size())
i = 0; i = 0;
} while (i != ii); } while (i != ii);
return false; return m_lemma_vec->size() > 0;
} }