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()); }