From 5e5f46f0f845f60e5226eadb6768de6fe4f528bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Jul 2018 17:34:45 -0700 Subject: [PATCH] handle cancelation from nra_solver gracefully Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context_pp.cpp | 2 ++ src/util/lp/nra_solver.cpp | 13 ++++++++++++- 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 3a2aacd26..623141038 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -419,6 +419,7 @@ namespace smt { visitor.collect(fmls); visitor.display_decls(out); visitor.display_asserts(out, fmls, true); + out << "(check-sat)\n"; } static unsigned g_lemma_id = 0; @@ -464,6 +465,7 @@ namespace smt { visitor.collect(fmls); visitor.display_decls(out); visitor.display_asserts(out, fmls, true); + out << "(check-sat)\n"; } void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp index b1ca67274..a4930b357 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/util/lp/nra_solver.cpp @@ -104,7 +104,18 @@ namespace nra { } // TBD: add variable bounds? - lbool r = m_nlsat->check(); + lbool r = l_undef; + try { + r = m_nlsat->check(); + } + catch (z3_exception&) { + if (m_limit.get_cancel_flag()) { + r = l_undef; + } + else { + throw; + } + } TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n");); switch (r) { case l_true: