fixes for #3376

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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) {

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;);

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;
         }