From c722962124946eb197f9ddab0cf718f85c2a4712 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2020 10:55:43 -0700 Subject: [PATCH] fix regressions in python API for user-propagator Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 910d89573..b5d33ff6c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10556,7 +10556,7 @@ def user_prop_fresh(id, ctx): def user_prop_fixed(ctx, cb, id, value): prop = _prop_closures.get(ctx) 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 def user_prop_final(ctx, cb): @@ -10684,7 +10684,7 @@ class UserPropagateBase: for i in range(num_eqs): _lhs[i] = eqs[i][0] _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): - self.propagate(ids, BoolVal(False, self.ctx_ref())) + self.propagate(BoolVal(False, self.ctx()), ids, eqs=[])