From adcb3e8f86c577603230a08c8eab18050ed966cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Jul 2022 20:27:50 -0700 Subject: [PATCH 1/3] set version number Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- scripts/mk_project.py | 2 +- scripts/nightly.yaml | 4 ++-- scripts/release.yml | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index cffe1a4d702..5217525356c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.9.2.0 LANGUAGES CXX) +project(Z3 VERSION 4.10.0.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 9f7a69b56c6..40624fc5d06 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 9, 2, 0) + set_version(4, 10, 0, 0) # Z3 Project definition def init_project_def(): diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index fd93d423652..552c811650f 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,8 +1,8 @@ variables: Major: '4' - Minor: '9' - Patch: '2' + Minor: '10' + Patch: '0' NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName) stages: diff --git a/scripts/release.yml b/scripts/release.yml index 419d4bc4b75..042eda657d0 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.9.2' + ReleaseVersion: '4.10.0' stages: From 907dc2c2d262b44aa210044af30a34daf898dac1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Jul 2022 20:45:45 -0700 Subject: [PATCH 2/3] adding toString() to model object Signed-off-by: Nikolaj Bjorner --- src/api/js/src/high-level/high-level.ts | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 489d4acdb0b..c4f315de954 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -1050,6 +1050,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return check(Z3.model_to_string(contextPtr, this.ptr)); } + toString() { + return this.sexpr(); + } + eval(expr: Bool, modelCompletion?: boolean): Bool; eval(expr: Arith, modelCompletion?: boolean): Arith; eval(expr: Expr, modelCompletion: boolean = false) { From 0f9684e1f81e206e020b09b51f2857c2ffe7f0e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Jul 2022 21:44:02 -0700 Subject: [PATCH 3/3] 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 11dcedbe808..9ce7a0531ab 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -204,12 +204,13 @@ def __init__(self, *args, **kws): 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)