From 8d0e66b3e371b2e0d54070e98813033c54bacb24 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 9 Apr 2024 11:16:34 -0700
Subject: [PATCH] fix regression introduced when testing

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

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 44f56efcd..216e03583 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1522,11 +1522,6 @@ lbool core::check() {
             return l_false;
     }
 
-    if (no_effect() && params().arith_nl_nra()) {
-        ret = m_nra.check();
-        lp_settings().stats().m_nra_calls++;
-    }
-
     
     if (no_effect() && should_run_bounded_nlsat()) 
         ret = bounded_nlsat();