From 2613f74baaa945806251594fea021ec4b4eb1d1f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 11 Jun 2020 00:05:19 -0700
Subject: [PATCH] fix #4494

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

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index e3cc00816..02f90e5a1 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1469,13 +1469,12 @@ lbool core::check(vector<lemma>& l_vec) {
 
     init_to_refine();
     patch_monomials();
+    set_use_nra_model(false);    
     if (m_to_refine.is_empty()) { return l_true; }   
     init_search();
 
     lbool ret = l_undef;
 
-    set_use_nra_model(false);    
-
     if (l_vec.empty() && !done()) 
         m_monomial_bounds();