diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3ff880b8e..a44a7659b 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2974,9 +2974,11 @@ public:
         else {
             ci = m_solver->add_var_bound(vi, k, b.get_value());
         }
+        if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
+            return;
+        }
         TRACE("arith", tout << "v" << b.get_var() << "\n";);
         add_ineq_constraint(ci, literal(bv, !is_true));
-
         propagate_eqs(vi, ci, k, b);
     }
 
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 274842909..6d298515a 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -839,12 +839,26 @@ struct solver::imp {
         m_expl->clear();
         m_lemma->clear();
     }
+
+    bool order_lemma(const unsigned_vector& to_refine) {
+        return false;
+    }
+
+    bool monotonicity_lemma(const unsigned_vector& to_refine) {
+        return false;
+    }
+
+    bool tangent_lemma(const unsigned_vector& to_refine) {
+        return false;
+    }
     
     lbool check(lp::explanation & exp, lemma& l) {
         TRACE("nla_solver", tout << "check of nla";);
         m_expl =   &exp;
         m_lemma =  &l;
-        lp_assert(m_lar_solver.get_status() == lp::lp_status::OPTIMAL);
+       
+        if (m_lar_solver.get_status() != lp::lp_status::OPTIMAL)
+            return l_undef;
         unsigned_vector to_refine;
         for (unsigned i = 0; i < m_monomials.size(); i++) {
             if (!check_monomial(m_monomials[i]))
@@ -857,14 +871,29 @@ struct solver::imp {
         TRACE("nla_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;);
         
         init_search();
-        
-        if (basic_lemma(to_refine)) {
-            return l_false;
-        }
-        
-        return l_undef;
+        for (int search_level = 0; search_level < 3; search_level++) {
+            if (search_level == 0) {
+                if (basic_lemma(to_refine)) {
+                    return l_false;
+                }
+            } else if (search_level == 1) {
+                if (order_lemma(to_refine)) {
+                    return l_false;
+                }
+            } else { // search_level == 3
+                if (monotonicity_lemma(to_refine)) {
+                    return l_false;
+                }
+                                
+                if (tangent_lemma(to_refine)) {
+                    return l_false;
+                }
+            }
     }
     
+    return l_undef;
+}
+    
     void test_factorization(unsigned mon_index, unsigned number_of_factorizations) {
         vector<ineq> lemma;
         m_lemma = & lemma;