diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 422947b1a..40adc33d2 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1246,7 +1246,9 @@ bool core::conflict_found() const {
 }
 
 bool core::done() const {
-    return m_lemma_vec->size() >= 10 || conflict_found();
+    return m_lemma_vec->size() >= 10 || 
+        conflict_found() || 
+        lp_settings().get_cancel_flag();
 }
 
 lbool core::incremental_linearization(bool constraint_derived) {
diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp
index a50df5ecb..1e9eae494 100644
--- a/src/math/lp/nla_tangent_lemmas.cpp
+++ b/src/math/lp/nla_tangent_lemmas.cpp
@@ -134,7 +134,7 @@ struct imp {
         SASSERT(plane_is_correct_cut(a));
         int steps = 10;
         point del = a - m_xy;
-        while (steps--) {
+        while (steps-- && !c().done()) {
             del *= rational(2);
             point na = m_xy + del;
             TRACE("nla_solver_tp", tout << "del = " << del << std::endl;);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3dbb81d36..0b88dd4e1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2280,6 +2280,7 @@ public:
         local_bound_propagator bp(*this);
 
         lp().propagate_bounds_for_touched_rows(bp);
+
         if (m.canceled()) {
             return;
         }