diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e76eaf0bb..95a97ea83 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1378,7 +1378,7 @@ class PythonInstallComponent(Component): MakeRuleCmd.make_install_directory(out, self.pythonPkgDir, in_prefix=self.in_prefix_install) # Sym-link or copy libz3 into python package directory - if IS_WINDOWS or self.is_osx_hack(): + if IS_WINDOWS or IS_OSX: MakeRuleCmd.install_files(out, self.libz3Component.dll_file(), os.path.join(self.pythonPkgDir, diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 8fdc795fb..09e4bd3a9 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -467,13 +467,8 @@ end = struct let to_string ( x : sort ) = Z3native.sort_to_string (gnc x) (gno x) let mk_uninterpreted ( ctx : context ) ( s : Symbol.symbol ) = - let res = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in - (z3obj_sno res ctx (Z3native.mk_uninterpreted_sort (context_gno ctx) (Symbol.gno s))) ; - (z3obj_create res) ; - Sort(res) + let n = (Z3native.mk_uninterpreted_sort (context_gno ctx) (Symbol.gno s)) in + Sort(z3_native_object_of_ast_ptr ctx n) let mk_uninterpreted_s ( ctx : context ) ( s : string ) = mk_uninterpreted ctx (Symbol.mk_string ( ctx : context ) s) @@ -537,22 +532,10 @@ end = struct let ast_of_func_decl f = match f with FuncDecl(x) -> x let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort list ) ( range : Sort.sort ) = - let res = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in - (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ; - (z3obj_create res) ; - FuncDecl(res) + func_decl_of_ptr ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (Sort.sort_lton domain) (Sort.gno range)) let create_pdr ( ctx : context) ( prefix : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) = - let res = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.inc_ref ; - dec_ref = Z3native.dec_ref } in - (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ; - (z3obj_create res) ; - FuncDecl(res) + func_decl_of_ptr ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (Sort.sort_lton domain) (Sort.gno range)) let gc ( x : func_decl ) = match x with FuncDecl(a) -> (z3obj_gc a) let gnc ( x : func_decl ) = match x with FuncDecl(a) -> (z3obj_gnc a)