diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 9c5fc1c8e..c45165d79 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -348,6 +348,7 @@ public: m_eq_eh = nullptr; m_diseq_eh = nullptr; m_created_eh = nullptr; + m_decide_eh = nullptr; } void user_propagate_init( @@ -385,6 +386,10 @@ public: void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { m_created_eh = created_eh; } + + void user_propagate_register_decide(user_propagator::decide_eh_t& decide_eh) override { + m_decide_eh = decide_eh; + } }; static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) { diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index fe89d6533..09ede0c35 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -116,8 +116,8 @@ public: m_tactic->user_propagate_register_created(created_eh); } - void user_propagate_register_decide(user_propagator::decide_eh_t& created_eh) override { - m_tactic->user_propagate_register_decide(created_eh); + void user_propagate_register_decide(user_propagator::decide_eh_t& decide_eh) override { + m_tactic->user_propagate_register_decide(decide_eh); } void user_propagate_clear() override {