mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
#5507 missing init
This commit is contained in:
parent
07c26208fa
commit
4d39af3d7b
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue