mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix the usage of sign flag

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-06 16:49:07 -07:00
parent 495161fe5c
commit b85b27d7bb
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_order_lemmas.cpp
View file

@ -268,7 +268,7 @@ void order::generate_ol(const monomial& ac,
rational rc_sign = rational(c_sign);
mk_ineq(rc_sign * canonize_sign(c), var(c), llc::LE);
mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp);
mk_ineq(canonize_sign(a)*rc_sign, var(a), - canonize_sign(b)*rc_sign, var(b), negate(ab_cmp));
mk_ineq(sign_to_rat(canonize_sign(a))*rc_sign, var(a), - sign_to_rat(canonize_sign(b))*rc_sign, var(b), negate(ab_cmp));
explain(ac);
explain(a);
explain(bc);