mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix in basic_lemma_for_mon_zero_model_based()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-06 19:27:43 -07:00
parent e9a4a60fbc
commit c35b561496
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/nla_basics_lemmas.cpp
View file

@ -496,7 +496,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const fact
TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
SASSERT(val(rm).is_zero()&& ! c().rm_check(rm)); SASSERT(val(rm).is_zero()&& ! c().rm_check(rm));
add_empty_lemma(); add_empty_lemma();
if (is_separated_from_zero(f)) { if (!is_separated_from_zero(f)) {
c().mk_ineq(var(rm), llc::NE); c().mk_ineq(var(rm), llc::NE);
for (auto j : f) { for (auto j : f) {
c().mk_ineq(var(j), llc::EQ); c().mk_ineq(var(j), llc::EQ);