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 bb59af04e0..351b3cb80a 100644
--- a/tools/common/consts.rs
+++ b/tools/common/consts.rs
@@ -1,4 +1,4 @@
-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";
 #[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 =