[Z3] Change z3 timeout to rlimit for determistic prove behavior

[kurisu6912]

As title. rlimit is like max_step in z3, designed to provide determistic behavior

Summary by CodeRabbit

• Chores
  • Updated internal dependency reference.

_{✏️ Tip: You can customize this high-level summary in your review settings.}

[github-actions]

👋 Hi! Thank you for contributing to the TileLang project.

Please remember to run pre-commit run --all-files in the root directory of the project to ensure your changes are properly linted and formatted. This will help ensure your contribution passes the format check.

We appreciate you taking this step! Our team will review your contribution, and we look forward to your awesome work! 🚀

[coderabbitai]

📝 Walkthrough

Walkthrough

The subproject pointer for the TVM dependency (3rdparty/tvm) has been updated to reference a new commit. The submodule now points to a different revision without any behavioral changes to the codebase itself.

Changes

Cohort / File(s)	Summary
Submodule Reference Update 3rdparty/tvm	Subproject pointer updated from commit 62af3338d60e5b026f35b99ce723604afacf2228 to b487ec4267d4890fddd7a5417e75b1a1fa553c06; no behavioral changes

Estimated code review effort

🎯 1 (Trivial) | ⏱️ ~2 minutes

Poem

🐰 A tiny tweak, a pointer changed with care,
New commit hash floating in the air,
TVM submodule, pointing fresh and true,
Dependencies dance—onwards we flew! 🚀

Pre-merge checks and finishing touches

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Title check	⚠️ Warning	The PR title mentions Z3 and rlimit/timeout, but the changeset only shows a TVM subproject pointer update with no behavioral changes to Z3 configuration.	Update the PR title to accurately reflect that this is a TVM submodule version bump, or verify that the actual Z3 configuration changes are present in the full changeset.

✅ Passed checks (2 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.

✨ Finishing touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Post copyable unit tests in a comment

---

📜 Recent review details

Configuration used: defaults

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 9b58ed0 and cae829a.

📒 Files selected for processing (1)

• 3rdparty/tvm

⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)

• GitHub Check: Test for Python 3.12 with Metal (on macos-latest)

🔇 Additional comments (1)

3rdparty/tvm (1)

1-1: Verify the Z3 timeout implementation in the TVM submodule commit.

The submodule pointer update is indirect: Z3 timeout behavior is controlled by tvm.arith.Analyzer.set_z3_timeout_ms(), so changes to the TVM submodule can affect Z3's proving behavior. However, the actual changes cannot be verified from this PR alone because:

• The TVM fork has limited commit history
• The target commit b487ec4267d4890fddd7a5417e75b1a1fa553c06 is not accessible in the current environment
• The specific implementation—whether it uses rlimit, timeout_ms, or another mechanism—remains unverified

To complete this review, inspect the TVM fork directly or provide the commit diff showing:

1. What changed in Z3's timeout implementation
2. Whether the change improves determinism
3. Any configuration updates or API changes required by dependents

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[kurisu6912]

@regression-perf

[LeiWang1999]

This bug of ci is not introduced by this pull request and will be fixed at #1543

[LeiWang1999]

@regression-perf

[github-actions]

Performance Benchmark Report

Triggered by: @LeiWang1999
Workflow run: https://github.com/tile-ai/tilelang/actions/runs/20524014368

Results

File	Original Latency	Current Latency	Speedup
sparse_mla_fwd_pipelined	0.136438	0.148064	0.92148
example_warp_specialize_gemm_barrierpipe_stage2	0.037664	0.039905	0.943842
sparse_mla_fwd	0.682899	0.712407	0.958581
example_warp_specialize_gemm_copy_0_gemm_1	0.038593	0.039809	0.969454
example_tilelang_gemm_fp8_2xAcc	0.186772	0.190548	0.980178
example_tilelang_gemm_fp8	0.0150085	0.015136	0.991576
example_dequant_gemm_fp4_hopper	0.012032	0.012097	0.994627
example_convolution	1.3193	1.32592	0.995006
example_tilelang_nsa_decode	0.00672115	0.00673878	0.997384
example_dequant_gemm_bf16_mxfp4_hopper	0.012256	0.012288	0.997396
example_mha_sink_fwd_bhsd	0.0124962	0.0125265	0.99758
example_dequant_gemm_bf16_fp4_hopper	0.014624	0.014657	0.997749
example_dequant_groupedgemm_bf16_mxfp4_hopper	0.0192856	0.0193239	0.998016
example_gqa_bwd_wgmma_pipelined	0.0735529	0.0736799	0.998278
example_group_per_split_token_cast_to_fp8	0.0102461	0.0102609	0.998559
example_tilelang_block_sparse_attn	0.00778891	0.00779473	0.999253
example_mla_decode	0.454891	0.45521	0.999299
example_gemm_schedule	0.0324124	0.0324314	0.999415
topk_selector	0.0536737	0.0536953	0.999599
example_mha_bwd_bhsd	0.0401058	0.0401207	0.999628
example_mha_sink_fwd_bhsd_sliding_window	0.0128477	0.0128523	0.999644
example_linear_attn_fwd	0.0363436	0.0363482	0.999872
example_gqa_bwd_tma_reduce_varlen	0.0635459	0.0635536	0.999879
example_fusedmoe_tilelang	0.145459	0.145468	0.999938
example_tilelang_gemm_splitk_vectorize_atomicadd	0.0492817	0.049284	0.999953
sparse_mla_bwd	0.380678	0.380681	0.999993
example_tilelang_gemm_fp8_intrinsic	0.002576	0.002576	1
example_topk	0.010912	0.010912	1
example_mha_sink_fwd_bhsd_wgmma_pipelined	0.0154335	0.0154317	1.00011
block_sparse_attn_tilelang	0.0102505	0.0102492	1.00013
example_vertical_slash_sparse_attn	0.23809	0.238037	1.00023
example_per_token_cast_to_fp8	0.00733178	0.00733008	1.00023
example_tilelang_nsa_fwd	0.0070364	0.00703461	1.00025
tilelang_example_sparse_tensorcore	0.0150439	0.0150389	1.00033
example_mha_fwd_varlen	0.0455895	0.0455731	1.00036
example_blocksparse_gemm	0.0225988	0.0225854	1.00059
example_gemv	0.0655582	0.065516	1.00064
example_mha_bwd_bshd_wgmma_pipelined	0.0257023	0.0256823	1.00078
example_mha_sink_fwd_bhsd_wgmma_pipelined_sliding_window	0.0154977	0.0154842	1.00087
example_mha_sink_bwd_bhsd_sliding_window	0.0327042	0.0326739	1.00093
example_gqa_bwd	0.0496879	0.0496362	1.00104
example_tilelang_sparse_gqa_decode_varlen_indice	0.0170373	0.017019	1.00108
example_tilelang_gemm_splitk	0.0493145	0.0492612	1.00108
fp8_lighting_indexer	0.0358412	0.0357965	1.00125
example_linear_attn_bwd	0.15175	0.15156	1.00125
example_gemm_autotune	0.022465	0.022433	1.00143
example_mha_bwd_bshd	0.040767	0.0407074	1.00147
example_elementwise_add	0.0222845	0.0222496	1.00157
example_dequant_gemv_fp16xint4	0.00376395	0.00375746	1.00173
example_tilelang_sparse_gqa_decode_varlen_mask	0.0232437	0.0232013	1.00183
example_convolution_autotune	0.996118	0.992316	1.00383
example_mha_sink_bwd_bhsd	0.0551947	0.0549503	1.00445
example_gemm_intrinsics	0.035169	0.035009	1.00457
example_mha_inference	0.0798289	0.0793403	1.00616
example_gemm	0.022977	0.022785	1.00843
example_gqa_decode	0.048289	0.047809	1.01004
example_dynamic	0.027968	0.027489	1.01743
example_gqa_sink_fwd_bhsd_wgmma_pipelined_sliding_window	0.0149847	0.0145919	1.02692
example_gqa_sink_fwd_bhsd_wgmma_pipelined	0.0148288	0.0144142	1.02876
example_warp_specialize_gemm_softpipe_stage2	0.039265	0.038017	1.03283
example_dequant_gemm_w4a8	0.005504	0.00528	1.04242
example_gqa_sink_bwd_bhsd	0.0432674	0.0414111	1.04483
example_gqa_sink_bwd_bhsd_sliding_window	0.0264823	0.0252607	1.04836
example_warp_specialize_gemm_copy_1_gemm_0	0.038848	0.036897	1.05288

Artifacts

• regression_result.png (speedup plot) is attached as a workflow artifact. Download it from the workflow run page above.