From bbb27775edcf3b27f0275abef9f1e166efe0f3cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Mar 2022 15:34:06 -0700 Subject: [PATCH] ensure that objects in callback are of sort Ast. --- src/api/python/z3/z3.py | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5e177ef08..6f4dcf430 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11252,35 +11252,38 @@ def user_prop_fresh(id, ctx): _prop_closures.set(new_prop.id, new_prop) return ctypes.c_void_p(new_prop.id) +def to_Ast(ptr,): + ast = Ast(ptr) + super(ctypes.c_void_p, ast).__init__(ptr) + return ast def user_prop_fixed(ctx, cb, id, value): prop = _prop_closures.get(ctx) prop.cb = cb - prop.fixed(_to_expr_ref(ctypes.c_void_p(id), prop.ctx()), _to_expr_ref(ctypes.c_void_p(value), prop.ctx())) + id = _to_expr_ref(to_Ast(id), prop.ctx()) + value = _to_expr_ref(to_Ast(value), prop.ctx()) + prop.fixed(id, value) prop.cb = None - def user_prop_final(ctx, cb): prop = _prop_closures.get(ctx) prop.cb = cb prop.final() prop.cb = None - def user_prop_eq(ctx, cb, x, y): prop = _prop_closures.get(ctx) prop.cb = cb - x = _to_expr_ref(ctypes.c_void_p(x), prop.ctx()) - y = _to_expr_ref(ctypes.c_void_p(y), prop.ctx()) + x = _to_expr_ref(to_Ast(x), prop.ctx()) + y = _to_expr_ref(to_Ast(y), prop.ctx()) prop.eq(x, y) prop.cb = None - def user_prop_diseq(ctx, cb, x, y): prop = _prop_closures.get(ctx) prop.cb = cb - x = _to_expr_ref(ctypes.c_void_p(x), prop.ctx()) - y = _to_expr_ref(ctypes.c_void_p(y), prop.ctx()) + x = _to_expr_ref(to_Ast(x), prop.ctx()) + y = _to_expr_ref(to_Ast(y), prop.ctx()) prop.diseq(x, y) prop.cb = None