From a38af61d777659e56afc97d9a8df2181e4a721bb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 Aug 2025 07:32:50 -0700
Subject: [PATCH] add call to check-assignment

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_core.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 5a74f882f..7795af30f 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1538,6 +1538,13 @@ lbool core::check() {
     if (no_effect()) 
         m_divisions.check();
 
+    bool use_nra_linearization = true;
+
+    if (no_effect() && use_nra_linearization) {
+        scoped_limits sl(m_reslim);
+        sl.push_child(&m_nra_lim);
+        ret = m_nra.check_assignment();
+    }
 
     if (no_effect()) {
         std::function<void(void)> check1 = [&]() { m_order.order_lemma();