mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 15:43:25 +00:00
Code Activity

make fresh_eh() work for Python bindings of user-propagator

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-21 21:44:02 -07:00
parent 907dc2c2d2
commit 0f9684e1f8
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/python/z3/z3.py
View file

@ -204,12 +204,13 @@ class Context:
Z3_set_param_value(conf, str(prev), _to_param_value(a)) Z3_set_param_value(conf, str(prev), _to_param_value(a))
prev = None prev = None
self.ctx = Z3_mk_context_rc(conf) self.ctx = Z3_mk_context_rc(conf)
self.owner = True
self.eh = Z3_set_error_handler(self.ctx, z3_error_handler) self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT) Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
Z3_del_config(conf) Z3_del_config(conf)
def __del__(self): 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) Z3_del_context(self.ctx)
self.ctx = None self.ctx = None
self.eh = None self.eh = None
@ -11367,12 +11368,14 @@ def user_prop_fresh(ctx, new_ctx):
_prop_closures.set_threaded() _prop_closures.set_threaded()
prop = _prop_closures.get(ctx) prop = _prop_closures.get(ctx)
nctx = Context() nctx = Context()
Z3_del_context(nctx.ctx)
new_ctx = to_ContextObj(new_ctx) new_ctx = to_ContextObj(new_ctx)
nctx.ctx = new_ctx nctx.ctx = new_ctx
nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler) nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler)
nctx.owner = False
new_prop = prop.fresh(nctx) new_prop = prop.fresh(nctx)
_prop_closures.set(new_prop.id, new_prop) _prop_closures.set(new_prop.id, new_prop)
return ctypes.c_void_p(new_prop.id) return new_prop.id
def to_Ast(ptr,): def to_Ast(ptr,):
ast = Ast(ptr) ast = Ast(ptr)