diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 40edf2fec69..d9c3d7011a6 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3882,8 +3882,9 @@ namespace z3 { public: - user_propagator_base(solver* s): s(s), c(nullptr) {} - user_propagator_base(Z3_context c): s(nullptr), c(c) {} + user_propagator_base(solver* s): s(s), c(nullptr) { + Z3_solver_propagate_init(ctx(), *s, push_eh, pop_eh, fresh_eh); + } virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0;