diff --git a/CMakeLists.txt b/CMakeLists.txt
index 3d183253b138..567edc1dc698 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -89,7 +89,7 @@ tvm_option(COMPILER_RT_PATH "Path to COMPILER-RT" "3rdparty/compiler-rt")
 # Contrib library options
 tvm_option(USE_BLAS "The blas library to be linked" none)
 tvm_option(USE_AMX "Enable Intel AMX" OFF)
-tvm_option(USE_Z3 "Build with Z3 SMT solver support" OFF)
+tvm_option(USE_Z3 "Build with Z3 SMT solver support" AUTO)
 tvm_option(USE_MKL "MKL root path when use MKL blas" OFF)
 tvm_option(USE_DNNL "Enable DNNL codegen" OFF)
 tvm_option(USE_CUDNN "Build with cuDNN" OFF)
diff --git a/ci/jenkins/docker-images.ini b/ci/jenkins/docker-images.ini
index 175ea8dded24..4681ecbc9bcd 100644
--- a/ci/jenkins/docker-images.ini
+++ b/ci/jenkins/docker-images.ini
@@ -17,7 +17,7 @@
 
 # This data file is read during when Jenkins runs job to determine docker images.
 [jenkins]
-ci_tag: 20260619-214849-4174cdf5
+ci_tag: 20260629-192919-24bbfd2e
 ci_arm: tlcpack/ci-arm:%(ci_tag)s
 ci_cpu: tlcpack/ci-cpu:%(ci_tag)s
 ci_gpu: tlcpack/ci-gpu:%(ci_tag)s
diff --git a/pyproject.toml b/pyproject.toml
index a4f80182cf11..3e83d4467121 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -16,7 +16,7 @@
 # under the License.
 
 [build-system]
-# z3-static ships the PIC static libz3 + headers for explicit USE_Z3=ON builds.
+# z3-static ships the PIC static libz3 + headers consumed by USE_Z3=ON.
 requires = [
   "scikit-build-core>=0.11",
   "setuptools-scm>=8",
@@ -146,8 +146,8 @@ logging.level = "INFO"
 [tool.scikit-build.cmake.define]
 TVM_BUILD_PYTHON_MODULE = "ON"
 USE_CUDA = "OFF"
-# Keep Z3 disabled by default until CI's C++ toolchain can link z3-static reliably.
-USE_Z3 = "OFF"
+# Statically link Z3 from the z3-static build dependency by default.
+USE_Z3 = "AUTO"
 BUILD_TESTING = "OFF"
 
 [tool.setuptools_scm]
diff --git a/src/arith/z3_prover.cc b/src/arith/z3_prover.cc
index 8aa066e2338b..037c47b41dca 100644
--- a/src/arith/z3_prover.cc
+++ b/src/arith/z3_prover.cc
@@ -556,8 +556,8 @@ class Z3Prover::Impl : ExprFunctor<z3::expr(const PrimExpr&)> {
   /// @brief Check if the expression type is supported by z3 integer operations.
   static bool IsZ3SupportedExpr(const PrimExprNode* expr) {
     TVM_FFI_DCHECK(expr != nullptr);
-    TVM_FFI_DCHECK(expr->ty.defined());
-    const auto* prim_ty = expr->ty.as<PrimTypeNode>();
+    TVM_FFI_DCHECK(expr->ty().defined());
+    const auto* prim_ty = expr->ty().as<PrimTypeNode>();
     TVM_FFI_DCHECK(prim_ty != nullptr);
     return (prim_ty->dtype.code == static_cast<uint8_t>(DLDataTypeCode::kDLInt) ||
             prim_ty->dtype.code == static_cast<uint8_t>(DLDataTypeCode::kDLUInt) ||