mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Update z3++.h

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-29 12:19:02 -07:00
parent 62fd22f555
commit ff723f15ff
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/c++/z3++.h
View file

@ -3927,7 +3927,7 @@ namespace z3 {
user_propagator_base(solver* s): s(s), c(nullptr) { user_propagator_base(solver* s): s(s), c(nullptr) {
Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh); Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
} }
virtual void push() = 0; virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0; virtual void pop(unsigned num_scopes) = 0;
@ -3948,13 +3948,13 @@ namespace z3 {
that were created using a solver. that were created using a solver.
*/ */
void fixed(fixed_eh_t& f) { void register_fixed(fixed_eh_t& f) {
assert(s); assert(s);
m_fixed_eh = f; m_fixed_eh = f;
Z3_solver_propagate_fixed(ctx(), *s, fixed_eh); Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
} }
void eq(eq_eh_t& f) { void register_eq(eq_eh_t& f) {
assert(s); assert(s);
m_eq_eh = f; m_eq_eh = f;
Z3_solver_propagate_eq(ctx(), *s, eq_eh); Z3_solver_propagate_eq(ctx(), *s, eq_eh);