From ca6839fc7aad311b11ca19a0e12afd538cb71e13 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Wed, 16 Feb 2022 18:22:37 +0100 Subject: [PATCH] Fixed bug in user-propagator "created" --- src/api/c++/z3++.h | 8 ++++---- src/smt/theory_user_propagator.cpp | 5 +++-- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a0d64bb736d..0bbab4185b4 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3939,10 +3939,6 @@ namespace z3 { Z3_solver_callback cb { nullptr }; - context& ctx() { - return c ? *c : s->ctx(); - } - struct scoped_cb { user_propagator_base& p; scoped_cb(void* _p, Z3_solver_callback cb):p(*static_cast(_p)) { @@ -4005,6 +4001,10 @@ namespace z3 { virtual ~user_propagator_base() = default; + context& ctx() { + return c ? *c : s->ctx(); + } + /** \brief user_propagators created using \c fresh() are created during search and their lifetimes are restricted to search time. They should diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index b95a98eddf2..85a02b154c9 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -101,6 +101,7 @@ theory * theory_user_propagator::mk_fresh(context * new_ctx) { if ((bool)m_final_eh) th->register_final(m_final_eh); if ((bool)m_eq_eh) th->register_eq(m_eq_eh); if ((bool)m_diseq_eh) th->register_diseq(m_diseq_eh); + if ((bool)m_created_eh) th->register_created(m_created_eh); return th; } @@ -228,8 +229,8 @@ bool theory_user_propagator::internalize_term(app* term) { add_expr(term); - if (!m_created_eh && (m_fixed_eh || m_eq_eh || m_diseq_eh)) - throw default_exception("You have to register a created event handler for new terms if you track them"); + if (!m_created_eh && (m_fixed_eh || m_eq_eh || m_diseq_eh)) + return true; if (m_created_eh) m_created_eh(m_user_context, this, term); return true;