From 4c5c17c7d82fb4d466f3800c1d74144a20e9a3b9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Mar 2020 11:07:51 -0700 Subject: [PATCH] fixes for #3376 Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 4 +++- src/math/lp/nla_tangent_lemmas.cpp | 2 +- src/smt/theory_lra.cpp | 1 + 3 files changed, 5 insertions(+), 2 deletions(-) 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; }