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

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 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 216e03583..449ecad4c 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1536,7 +1536,7 @@ lbool core::check() {
         m_divisions.check();
 
 
-    if (false && no_effect()) {
+    if (no_effect()) {
         std::function<void(void)> check1 = [&]() { m_order.order_lemma();
         };
         std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma();