update z3 to 4.14.0

source/tools/get-z3.ps1

@@ -1,4 +1,4 @@
-$z3_version = "4.12.5"
+$z3_version = "4.14.0"
 $filename = "z3-$z3_version-x64-win"
 
 $download_url = "https://github.com/Z3Prover/z3/releases/download/z3-$z3_version/$filename.zip"

source/tools/get-z3.sh

@@ -1,21 +1,22 @@
 #! /bin/bash -eu
 
-z3_version="4.12.5"
+# Should keep track of verus/tools/common/consts.rs
+z3_version="4.14.0"
 
 if [ `uname` == "Darwin" ]; then
     if [[ $(uname -m) == 'arm64' ]]; then
-        filename="z3-$z3_version-arm64-osx-11.0"
+        filename="z3-$z3_version-arm64-osx-13.7.2"
     elif [[ $(uname -m) == 'x86_64' ]]; then
-        filename="z3-$z3_version-x64-osx-11.7.10"
+        filename="z3-$z3_version-x64-osx-13.7.2"
     else
         echo "Unsupported architecture $(uname -m)"
         exit -1
     fi
 elif [ `uname` == "Linux" ]; then
     if [[ $(uname -m) == 'aarch64' ]]; then
-        filename="z3-$z3_version-arm64-glibc-2.35"
+        filename="z3-$z3_version-arm64-glibc-2.34"
     elif [[ $(uname -m) == 'x86_64' ]]; then
-        filename="z3-$z3_version-x64-glibc-2.31"
+        filename="z3-$z3_version-x64-glibc-2.35"
     else
         echo "Unsupported architecture $(uname -m)"
         exit -1

tools/common/consts.rs

@@ -1,4 +1,4 @@
-pub const EXPECTED_Z3_VERSION: &str = "4.12.5";
+pub const EXPECTED_Z3_VERSION: &str = "4.14.0";
 pub const EXPECTED_CVC5_VERSION: &str = "1.1.2";
 #[allow(dead_code)] // actually used in `rust_verify/util.rs`, but missed by the dead code checker, possibly due to the use of `#[path(...)]` for this file
 pub const VERUS_GITHUB_BUG_REPORT_URL: &str =