From 1ecc6a21fabcc94243bd034c41884b427b56990c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 May 2020 11:21:15 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_basics_lemmas.cpp | 4 ++-- src/math/lp/nla_core.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index f43539577..4de3674da 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -764,8 +764,8 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f) // x = 0 or y = 0 -> xy = 0 void basics::basic_lemma_for_mon_non_zero_model_based(const monic& rm, const factorization& f) { TRACE("nla_solver_bl", c().trace_print_monic_and_factorization(rm, f, tout);); -# NSB code review: -# the two branches are the same +// NSB code review: +// the two branches are the same if (f.is_mon()) basic_lemma_for_mon_non_zero_model_based_mf(f); else diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 8ca9d7cc7..c3a80309d 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -487,7 +487,7 @@ void core::mk_ineq(const rational& a, lpvar j, llc cmp) { mk_ineq(a, j, cmp, rational::zero()); } -void core::mk_ineq(lpvar j, lpvar k, llc cmp, lemma& l) { +void core::mk_ineq(lpvar j, lpvar k, llc cmp, lemma& _l) { mk_ineq(rational(1), j, rational(1), k, cmp, rational::zero()); }