mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 06:39:02 +00:00
Code Activity

fix in order lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-12 12:08:06 -10:00 committed by Lev Nachmanson
parent 47d7331dd5
commit dbfa3fc84a
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1003,6 +1003,7 @@ struct solver::imp {
int d_sign,
const factor& d,
lp::lconstraint_kind ab_cmp) {
mk_ineq(rational(c_sign) * flip_sign(c), var(c), lp::lconstraint_kind::LE);
negate_factor_equality(c, d);
negate_factor_relation(rational(c_sign), a, rational(d_sign), b);
mk_ineq(flip_sign(ac), var(ac), -flip_sign(bd), var(bd), ab_cmp);
@ -1012,6 +1013,7 @@ struct solver::imp {
explain(bd);
explain(b);
explain(d); // todo: double check that these explanations are enough!
TRACE("nla_solver", print_lemma(tout););
}
bool get_cd_signs_for_ol(const rational& c, const rational& d, int& c_sign, int & d_sign) const {