mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

generate lemma for proportional_case_ge

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-27 11:05:40 -07:00 • committed by Lev Nachmanson
parent 4deccebeb4
commit a1f572d55a
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_solver.cpp
View file

@ -1171,7 +1171,7 @@ struct solver::imp {
t.clear(); // abs(xy) - abs(y) <= 0
t.add_coeff_var(rational(xy_sign), xy);
t.add_coeff_var(rational(-y_sign), y);
m_lemma->push_back(ineq(lp::lconstraint_kind::LE, t, rational::zero()));
m_lemma->push_back(ineq(lp::lconstraint_kind::GE, t, rational::zero()));
TRACE("nla_solver", tout<< "lemma: ";print_lemma(*m_lemma, tout););
return true;
}