From 7f5427b839153279a943eecab347b266d687dffe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 30 May 2025 14:47:31 +0100
Subject: [PATCH] disable assertion that checks nl lemmas if using nra core

---
 src/math/lp/nla_core.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 3f16f32b6..6acc2b043 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1047,7 +1047,7 @@ new_lemma::new_lemma(core& c, char const* name):name(name), c(c) {
 new_lemma& new_lemma::operator|=(ineq const& ineq) {
     if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
         CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";);
-        SASSERT(!c.ineq_holds(ineq));
+        SASSERT(c.m_use_nra_model || !c.ineq_holds(ineq));
         current().push_back(ineq);
     }
     return *this;