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

fix regressions in python API for user-propagator

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-24 10:55:43 -07:00
parent e46ad45968
commit c722962124
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/python/z3/z3.py
View file

@ -10556,7 +10556,7 @@ def user_prop_fresh(id, ctx):
def user_prop_fixed(ctx, cb, id, value): def user_prop_fixed(ctx, cb, id, value):
prop = _prop_closures.get(ctx) prop = _prop_closures.get(ctx)
prop.cb = cb prop.cb = cb
prop.fixed(id, _to_expr_ref(ctypes.c_void_p(value), prop.ctx)) prop.fixed(id, _to_expr_ref(ctypes.c_void_p(value), prop.ctx()))
prop.cb = None prop.cb = None
def user_prop_final(ctx, cb): def user_prop_final(ctx, cb):
@ -10684,7 +10684,7 @@ class UserPropagateBase:
for i in range(num_eqs): for i in range(num_eqs):
_lhs[i] = eqs[i][0] _lhs[i] = eqs[i][0]
_rhs[i] = eqs[i][1] _rhs[i] = eqs[i][1]
Z3_solver_propagate_consequence(self.ctx_ref(), ctypes.c_void_p(self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast) Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
def conflict(self, ids): def conflict(self, ids):
self.propagate(ids, BoolVal(False, self.ctx_ref())) self.propagate(BoolVal(False, self.ctx()), ids, eqs=[])