From 7e4b232ac478184d3c457db8c52879dc149f43a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 May 2020 10:36:14 -0700 Subject: [PATCH] fix comment 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 eaa470db5..77bd16e0f 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -323,7 +323,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, } /* given: sign * m = ab - lemma b != val(b) || sign 0 m <= a*val(b) + lemma b != val(b) || sign*m <= a*val(b) */ void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) { if (!c().var_is_int(b) && val(b).is_big())