From 0f9684e1f81e206e020b09b51f2857c2ffe7f0e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Jul 2022 21:44:02 -0700 Subject: [PATCH] make fresh_eh() work for Python bindings of user-propagator --- src/api/python/z3/z3.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 11dcedbe8..9ce7a0531 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -204,12 +204,13 @@ class Context: Z3_set_param_value(conf, str(prev), _to_param_value(a)) prev = None self.ctx = Z3_mk_context_rc(conf) + self.owner = True self.eh = Z3_set_error_handler(self.ctx, z3_error_handler) Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT) Z3_del_config(conf) def __del__(self): - if Z3_del_context is not None: + if Z3_del_context is not None and self.owner: Z3_del_context(self.ctx) self.ctx = None self.eh = None @@ -11367,12 +11368,14 @@ def user_prop_fresh(ctx, new_ctx): _prop_closures.set_threaded() prop = _prop_closures.get(ctx) nctx = Context() + Z3_del_context(nctx.ctx) new_ctx = to_ContextObj(new_ctx) nctx.ctx = new_ctx nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler) + nctx.owner = False new_prop = prop.fresh(nctx) _prop_closures.set(new_prop.id, new_prop) - return ctypes.c_void_p(new_prop.id) + return new_prop.id def to_Ast(ptr,): ast = Ast(ptr)