[CI] Bump CI at the Ubuntu 24.04 images and re-enable USE_Z3

[tlopex]

This pr switches CI to the Ubuntu 24.04 (noble) images. Bump ci_tag in ci/jenkins/docker-images.ini to 20260629-192919-24bbfd2e -- the images built from #19893 (ci_cpu/ci_arm/ci_wasm/ci_gpu on Ubuntu 24.04, whose default g++ is gcc-13, giving full C++20 support).

Also, this pr re-enables Z3 (AUTO). #19828 temporarily set USE_Z3=OFF (in CMakeLists.txt and the pyproject wheel build) to dodge a z3-static build failure. The CI image now ships z3-static (#19835), so this restores USE_Z3=AUTO: the Z3-backed Analyzer proving is enabled when z3-static is available and silently skipped otherwise.

While Z3 stayed disabled, PrimExprNode::ty became a method, leaving two stale field accesses in z3_prover.cc's IsZ3SupportedExpr (only compiled under TVM_USE_Z3). Fixed expr->ty -> expr->ty().

Verification:

• The Ubuntu 24.04 images ([CI][Docker] Move CI images to Ubuntu 24.04 (noble) #19893) built successfully for ci_cpu/ci_arm/ ci_wasm/ci_gpu (the GPU image includes ROCm 6.4.4 and the CUDA 24.04 base).
• Re-enabling Z3 was validated with a build-only wheel run: all four wheels (Linux x86_64/aarch64 manylinux_2_28, macOS arm64, Windows) build green with z3-static compiled and linked, confirming the earlier z3-static link concern is resolved on the current toolchain.

[gemini-code-assist]

Code Review

This pull request changes the default Z3 SMT solver support setting to AUTO and updates the CI docker image tag. In src/arith/z3_prover.cc, the code is updated to use expr->ty() instead of expr->ty. The review comment correctly identifies a critical Use-After-Free (UAF) vulnerability introduced by this change, as calling .as<PrimTypeNode>() on the temporary Type object returned by expr->ty() results in a dangling pointer. Storing the returned Type in a local variable is recommended to ensure it remains alive during the check.

Important

The consumer version of Gemini Code Assist on GitHub is being sunset. Starting June 18, 2026, new organization installations will be blocked, and all code review activity will officially cease on July 17, 2026.
For more details on the timeline and next steps, please review the Help Documentation.

[gemini-code-assist]

Calling expr->ty() returns a temporary Type (or PrimType) object by value. Calling .as<PrimTypeNode>() directly on this temporary returns a raw pointer (const PrimTypeNode*) to the underlying node, but the temporary Type object itself is destroyed at the end of the statement (the semicolon).

If the PrimExprNode does not hold a strong reference to this specific PrimTypeNode instance (e.g., if ty() constructs the PrimType on the fly, which is common in TVM), the reference count of the PrimTypeNode drops to 0 and it is deallocated immediately. This leaves prim_ty as a dangling pointer, leading to a Use-After-Free (UAF) bug when prim_ty is accessed on the subsequent lines.

To fix this, store the returned Type object in a local variable to keep it alive for the duration of the function.

    auto ty = expr->ty();
    TVM_FFI_DCHECK(ty.defined());
    const auto* prim_ty = ty.as<PrimTypeNode>();

[tlopex]

@tvm-bot rerun