From 41aa7d7b60913ec17a50df8f998d2ca773070ac8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Dec 2021 09:00:51 -0800 Subject: [PATCH] stack Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 13 +++++-------- src/api/api_context.h | 2 +- 2 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 0f2473956..66a1384f5 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -87,8 +87,6 @@ namespace api { m_error_code = Z3_OK; m_print_mode = Z3_PRINT_SMTLIB_FULL; - - m_interruptable = nullptr; m_error_handler = &default_error_handler; m_bv_fid = m().mk_family_id("bv"); @@ -98,7 +96,7 @@ namespace api { m_datalog_fid = m().mk_family_id("datalog_relation"); m_fpa_fid = m().mk_family_id("fpa"); m_seq_fid = m().mk_family_id("seq"); - m_char_fid = m().mk_family_id("char"); + m_char_fid = m().mk_family_id("char"); m_special_relations_fid = m().mk_family_id("specrels"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); @@ -120,19 +118,18 @@ namespace api { context::set_interruptable::set_interruptable(context & ctx, event_handler & i): m_ctx(ctx) { lock_guard lock(ctx.m_mux); - SASSERT(m_ctx.m_interruptable == 0); - m_ctx.m_interruptable = &i; + m_ctx.m_interruptable.push_back(& i); } context::set_interruptable::~set_interruptable() { lock_guard lock(m_ctx.m_mux); - m_ctx.m_interruptable = nullptr; + m_ctx.m_interruptable.pop_back(); } void context::interrupt() { lock_guard lock(m_mux); - if (m_interruptable) - (*m_interruptable)(API_INTERRUPT_EH_CALLER); + for (auto * eh : m_interruptable) + (*eh)(API_INTERRUPT_EH_CALLER); m_limit.cancel(); m().limit().cancel(); } diff --git a/src/api/api_context.h b/src/api/api_context.h index ae9671f7a..41c797163 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -115,7 +115,7 @@ namespace api { std::string m_exception_msg; // catch the message associated with a Z3 exception Z3_ast_print_mode m_print_mode; - event_handler * m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt + ptr_vector m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt public: // Scoped obj for setting m_interruptable