diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 9b67b5d81..8f3a6ee0f 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -501,7 +501,7 @@ public: } void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { - m_ctx->user_propagate_register_created(created_eh); + m_created_eh = created_eh; } }; diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 15c9cab82..6ed570297 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -112,6 +112,10 @@ public: return m_tactic->user_propagate_register_expr(e); } + void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { + m_tactic->user_propagate_register_created(created_eh); + } + void user_propagate_clear() override { if (m_tactic) m_tactic->user_propagate_clear();