From fb0740aad40ab91eec23c17509d583cf717bf247 Mon Sep 17 00:00:00 2001
From: Catoverflow <55503205+Catoverflow@users.noreply.github.com>
Date: Wed, 23 Oct 2024 11:14:42 -0500
Subject: [PATCH] update default z3 version to 4.13.0

---
 source/air/src/smt_verify.rs | 2 +-
 source/tools/get-z3.ps1      | 2 +-
 source/tools/get-z3.sh       | 3 ++-
 tools/common/consts.rs       | 2 +-
 4 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/source/air/src/smt_verify.rs b/source/air/src/smt_verify.rs
index 84bd60c63c..9c50353e3a 100644
--- a/source/air/src/smt_verify.rs
+++ b/source/air/src/smt_verify.rs
@@ -183,7 +183,7 @@ pub(crate) fn smt_check_assertion<'ctx>(
             if let Some(expected_version) = &context.expected_solver_version {
                 let value: &str = &line[GET_VERSION_RESPONSE_PREFIX.len()..line.len() - 1];
                 let version = value.trim_matches(&[' ', '"'][..]);
-                if version != expected_version.as_str() {
+                if !version.starts_with(expected_version.as_str()) {
                     diagnostics.report(
                         &context
                             .message_interface
diff --git a/source/tools/get-z3.ps1 b/source/tools/get-z3.ps1
index dd6425e334..b117d15ece 100644
--- a/source/tools/get-z3.ps1
+++ b/source/tools/get-z3.ps1
@@ -1,4 +1,4 @@
-$z3_version = "4.12.5"
+$z3_version = "4.13.0"
 $filename = "z3-$z3_version-x64-win"
 
 $download_url = "https://github.com/Z3Prover/z3/releases/download/z3-$z3_version/$filename.zip"
diff --git a/source/tools/get-z3.sh b/source/tools/get-z3.sh
index 8a853f4286..213b983347 100755
--- a/source/tools/get-z3.sh
+++ b/source/tools/get-z3.sh
@@ -1,6 +1,7 @@
 #! /bin/bash -eu
 
-z3_version="4.12.5"
+# Should keep track of verus/tools/common/consts.rs
+z3_version="4.13.0"
 
 if [ `uname` == "Darwin" ]; then
     if [[ $(uname -m) == 'arm64' ]]; then
diff --git a/tools/common/consts.rs b/tools/common/consts.rs
index 4f6ab380db..594603f424 100644
--- a/tools/common/consts.rs
+++ b/tools/common/consts.rs
@@ -1,2 +1,2 @@
-pub const EXPECTED_Z3_VERSION: &str = "4.12.5";
+pub const EXPECTED_Z3_VERSION: &str = "4.13.0";
 pub const EXPECTED_CVC5_VERSION: &str = "1.1.2";