mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

a bug fix in simple sign lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2019-02-10 15:55:41 -08:00 • committed by Lev Nachmanson
parent 286cebd9db
commit 4243bd3e2a
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2312,7 +2312,7 @@ struct solver::imp {
} }
} }
mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT), current_lemma()); mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT), current_lemma());
TRACE("nla_solver", print_lemma_and_expl(tout);); TRACE("nla_solver", print_lemma_and_expl(tout););
} }
bool generate_simple_tangent_lemma(const rooted_mon* rm) { bool generate_simple_tangent_lemma(const rooted_mon* rm) {
@ -2325,7 +2325,7 @@ struct solver::imp {
SASSERT(!mv.is_zero() && !v.is_zero()); SASSERT(!mv.is_zero() && !v.is_zero());
rational sign = rational(rat_sign(mv)); rational sign = rational(rat_sign(mv));
if (sign != rat_sign(v)) { if (sign != rat_sign(v)) {
generate_simple_sign_lemma(sign, m); generate_simple_sign_lemma(-sign, m);
return true; return true;
} }
bool gt = abs(mv) > abs(v); bool gt = abs(mv) > abs(v);