Fixed bug in user-propagator "created" (#5843)

Z3Prover · Feb 16, 2022 · de0d9ce · de0d9ce
1 parent aa85e48
commit de0d9ce
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git 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<user_propagator_base*>(_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
@@ -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;