From b85b27d7bbddf58960abbd4a6cc4842d53cfb8c0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 May 2019 16:49:07 -0700 Subject: [PATCH] fix the usage of sign flag Signed-off-by: Lev Nachmanson --- src/util/lp/nla_order_lemmas.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp index 0fd458290..8f521f684 100644 --- a/src/util/lp/nla_order_lemmas.cpp +++ b/src/util/lp/nla_order_lemmas.cpp @@ -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);