From d6848175eb0bce38a8cdeec04e967f61cadacffc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Aug 2021 18:12:40 -0700 Subject: [PATCH] re-add API for creating propagator from a context for "fresh" --- src/api/c++/z3++.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 96302eb417c..8dd7f69437b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3882,9 +3882,11 @@ namespace z3 { public: + user_propagator_base(context* c) : s(nullptr), c(c) {} + user_propagator_base(solver* s): s(s), c(nullptr) { Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh); - } + } virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0;