[z3] Update to 4.8.16 (#24407)

* [z3] Update to 4.8.16

* Use Python3 instead of Python2

Python2 is EOL and the build script works with Python3, so we should
prefer Python3

* Update version

ports/z3/fix-32-bit-build.patch

@@ -1,132 +0,0 @@
-From 3828130791bf8e60038b46b0d6602cb7e43fb344 Mon Sep 17 00:00:00 2001
-From: Nikolaj Bjorner <nbjorner@microsoft.com>
-Date: Thu, 24 Mar 2022 14:05:05 -1000
-Subject: [PATCH] fix #5922 use 0u to help type inference
-
-Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
----
- src/api/c++/z3++.h | 30 +++++++++++++++---------------
- 1 file changed, 15 insertions(+), 15 deletions(-)
-
-diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
-index b00a33ad71..4d60de4338 100644
---- a/src/api/c++/z3++.h
-+++ b/src/api/c++/z3++.h
-@@ -2333,7 +2333,7 @@ namespace z3 {
- 
-     inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
-         assert(es.size() > 0);
--        context& ctx = es[0].ctx();
-+        context& ctx = es[0u].ctx();
-         array<Z3_ast> _es(es);
-         Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
-         ctx.check_error();
-@@ -2341,7 +2341,7 @@ namespace z3 {
-     }
-     inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
-         assert(es.size() > 0);
--        context& ctx = es[0].ctx();
-+        context& ctx = es[0u].ctx();
-         array<Z3_ast> _es(es);
-         Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
-         ctx.check_error();
-@@ -2349,7 +2349,7 @@ namespace z3 {
-     }
-     inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
-         assert(es.size() > 0);
--        context& ctx = es[0].ctx();
-+        context& ctx = es[0u].ctx();
-         array<Z3_ast> _es(es);
-         Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
-         ctx.check_error();
-@@ -2357,7 +2357,7 @@ namespace z3 {
-     }
-     inline expr atmost(expr_vector const& es, unsigned bound) {
-         assert(es.size() > 0);
--        context& ctx = es[0].ctx();
-+        context& ctx = es[0u].ctx();
-         array<Z3_ast> _es(es);
-         Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
-         ctx.check_error();
-@@ -2365,7 +2365,7 @@ namespace z3 {
-     }
-     inline expr atleast(expr_vector const& es, unsigned bound) {
-         assert(es.size() > 0);
--        context& ctx = es[0].ctx();
-+        context& ctx = es[0u].ctx();
-         array<Z3_ast> _es(es);
-         Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
-         ctx.check_error();
-@@ -2373,7 +2373,7 @@ namespace z3 {
-     }
-     inline expr sum(expr_vector const& args) {
-         assert(args.size() > 0);
--        context& ctx = args[0].ctx();
-+        context& ctx = args[0u].ctx();
-         array<Z3_ast> _args(args);
-         Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
-         ctx.check_error();
-@@ -2382,7 +2382,7 @@ namespace z3 {
- 
-     inline expr distinct(expr_vector const& args) {
-         assert(args.size() > 0);
--        context& ctx = args[0].ctx();
-+        context& ctx = args[0u].ctx();
-         array<Z3_ast> _args(args);
-         Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
-         ctx.check_error();
-@@ -2411,14 +2411,14 @@ namespace z3 {
-         Z3_ast r;
-         assert(args.size() > 0);
-         if (args.size() == 1) {
--            return args[0];
-+            return args[0u];
-         }
--        context& ctx = args[0].ctx();
-+        context& ctx = args[0u].ctx();
-         array<Z3_ast> _args(args);
--        if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
-+        if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
-             r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
-         }
--        else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
-+        else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
-             r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
-         }
-         else {
-@@ -2448,7 +2448,7 @@ namespace z3 {
-     inline expr mk_xor(expr_vector const& args) {
-         if (args.empty())
-             return args.ctx().bool_val(false);
--        expr r = args[0];
-+        expr r = args[0u];
-         for (unsigned i = 1; i < args.size(); ++i)
-             r = r ^ args[i];
-         return r;
-@@ -2771,7 +2771,7 @@ namespace z3 {
-                 assert(!m_end && !m_empty);
-                 m_cube = m_solver.cube(m_vars, m_cutoff);
-                 m_cutoff = 0xFFFFFFFF;
--                if (m_cube.size() == 1 && m_cube[0].is_false()) {
-+                if (m_cube.size() == 1 && m_cube[0u].is_false()) {
-                     m_cube = z3::expr_vector(m_solver.ctx());
-                     m_end = true;
-                 }
-@@ -3005,7 +3005,7 @@ namespace z3 {
-         }
-         array<Z3_tactic> buffer(n);
-         for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
--        return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
-+        return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
-     }
- 
-     inline tactic par_and_then(tactic const & t1, tactic const & t2) {
-@@ -3804,7 +3804,7 @@ namespace z3 {
-     }
-     inline expr re_intersect(expr_vector const& args) {
-         assert(args.size() > 0);
--        context& ctx = args[0].ctx();
-+        context& ctx = args[0u].ctx();
-         array<Z3_ast> _args(args);
-         Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
-         ctx.check_error();

ports/z3/portfile.cmake

@@ -1,17 +1,16 @@
-vcpkg_find_acquire_program(PYTHON2)
+vcpkg_find_acquire_program(PYTHON3)
-get_filename_component(PYTHON2_DIR "${PYTHON2}" DIRECTORY)
+get_filename_component(PYTHON3_DIR "${PYTHON3}" DIRECTORY)
-vcpkg_add_to_path("${PYTHON2_DIR}")
+vcpkg_add_to_path("${PYTHON3_DIR}")
 
 vcpkg_from_github(
   OUT_SOURCE_PATH SOURCE_PATH
   REPO Z3Prover/z3
-  REF z3-4.8.15
+  REF z3-4.8.16
-  SHA512 7b08dec5b035a38edc90c4c491f508fd9ed227357de94400169db53d4c59382bd6a81ae6615771023a06534a3aa92668844f0ebfcc2a3b5ef4bba957426a0c6c
+  SHA512 385f6e1ee075b9eadb5aad338657a81f518eef382b99ce623448a630b79f5d414ebccfd1bb5e959626f0b82ef54a5f20326814ae988b5688d51578de6fb69615
   HEAD_REF master
   PATCHES
       fix-install-path.patch
       remove-flag-overrides.patch
-      fix-32-bit-build.patch
 )
 
 if (VCPKG_LIBRARY_LINKAGE STREQUAL "static")

ports/z3/remove-flag-overrides.patch

@@ -7,6 +7,6 @@ index 477410ba8..fcca03917 100644
  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.8.15.0 LANGUAGES CXX)
+ project(Z3 VERSION 4.8.16.0 LANGUAGES CXX)
  
  ################################################################################

ports/z3/vcpkg.json

@@ -1,6 +1,6 @@
 {
   "name": "z3",
-  "version": "4.8.15",
+  "version": "4.8.16",
   "description": "Z3 is a theorem prover from Microsoft Research",
   "homepage": "https://github.com/Z3Prover/z3",
   "license": "MIT",

versions/baseline.json

@@ -7665,7 +7665,7 @@
       "port-version": 0
     },
     "z3": {
-      "baseline": "4.8.15",
+      "baseline": "4.8.16",
       "port-version": 0
     },
     "z85": {

versions/z-/z3.json

@@ -1,5 +1,10 @@
 {
   "versions": [
+    {
+      "git-tree": "a1217f07ef4a8f918f5b61a01057a4ee70f92422",
+      "version": "4.8.16",
+      "port-version": 0
+    },
     {
       "git-tree": "ca14e43533889ce4abf89af387b73d015e133c4a",
       "version": "4.8.15",