From 318d7d7564425ed003d6a342f8c77a0885b838ee Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 1 Sep 2023 11:32:26 -0700 Subject: [PATCH] fixes a bug --- src/math/lp/nla_core.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 622475cf4..4d4fa6cbe 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1058,10 +1058,7 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) { } // Contrary to new_lemma::operator|=, this method does not assert that the model does not satisfy the ineq. -// If ineq holds then it is a nop. new_lemma& new_lemma::operator+=(ineq const& ineq) { - if (c.ineq_holds(ineq)) return *this; - if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) { current().push_back(ineq); }