Skip to content

Commit

Permalink
re-add API for creating propagator from a context for "fresh"
Browse files Browse the repository at this point in the history
  • Loading branch information
NikolajBjorner committed Aug 27, 2021
1 parent f7c1ed8 commit d684817
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/api/c++/z3++.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down

0 comments on commit d684817

Please sign in to comment.