From 754bafc95eaa6257b34a8e2c7565ff7f1920b663 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 May 2020 13:54:52 -0700 Subject: [PATCH] fix #4267 Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_order_lemmas.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 92333454f..91612e4a9 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -266,7 +266,7 @@ void order::generate_ol_eq(const monic& ac, // ac == bc lemma |= ineq(c.var(), llc::EQ, 0); // c is not equal to zero lemma |= ineq(term(ac.var(), -rational(1), bc.var()), llc::NE, 0); - lemma |= ineq(term(rational(canonize_sign(a)), a.var(), rational(!canonize_sign(b)), b.var()), llc::EQ, 0); + lemma |= ineq(term(sign_to_rat(canonize_sign(a)), a.var(), sign_to_rat(!canonize_sign(b)), b.var()), llc::EQ, 0); lemma &= ac; lemma &= a; lemma &= bc;