diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 11652dd26..def72518f 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1506,12 +1506,11 @@ lbool core::check(vector<lemma>& l_vec) {
             m_tangents.tangent_lemma();
     }
 
-
     if (!m_reslim.inc())
         return l_undef;
   
- finish_up:   
     lbool ret = l_vec.empty() ? l_undef : l_false;
+
 #if 0
     if (l_vec.empty()) 
         ret = m_nra.check();