From a1f572d55a77b2296f8a88297ac7549970517eea Mon Sep 17 00:00:00 2001 From: Lev Date: Thu, 27 Sep 2018 11:05:40 -0700 Subject: [PATCH] generate lemma for proportional_case_ge Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index b33584bde..0fb02a039 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -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; }