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