diff --git a/.github/workflows/build-warning-fixer.lock.yml b/.github/workflows/build-warning-fixer.lock.yml
index d866702070..5d50311206 100644
--- a/.github/workflows/build-warning-fixer.lock.yml
+++ b/.github/workflows/build-warning-fixer.lock.yml
@@ -1,4 +1,4 @@
-# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"8e86ba4261f8c71ab0e24c7d0bc7edf67727e4be5859ff2fdaf6678076207eab","body_hash":"8922ba3a21444e84982af2576e34d4b4ef553ca0655a384c58f9d05712e92a11","compiler_version":"v0.83.4","strict":true,"agent_id":"copilot","engine_versions":{"copilot":"1.0.75"}}
+# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"c65096f8348ac1ac5c1314ec367754e2d60976068118951cd31a640508c4eeaa","body_hash":"459dd7fdb2ee5a282dc3a85286a93073c174486bb276b542bd13dc12373423f0","compiler_version":"v0.83.4","strict":true,"agent_id":"copilot","engine_versions":{"copilot":"1.0.75"}}
 # gh-aw-manifest: {"version":1,"secrets":["COPILOT_GITHUB_TOKEN","GH_AW_CI_TRIGGER_TOKEN","GH_AW_GITHUB_MCP_SERVER_TOKEN","GH_AW_GITHUB_TOKEN","GITHUB_TOKEN"],"actions":[{"repo":"actions/cache/restore","sha":"55cc8345863c7cc4c66a329aec7e433d2d1c52a9","version":"v6.1.0"},{"repo":"actions/cache/save","sha":"55cc8345863c7cc4c66a329aec7e433d2d1c52a9","version":"v6.1.0"},{"repo":"actions/checkout","sha":"3d3c42e5aac5ba805825da76410c181273ba90b1","version":"v7.0.1"},{"repo":"actions/download-artifact","sha":"3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c","version":"v8.0.1"},{"repo":"actions/github-script","sha":"3a2844b7e9c422d3c10d287c895573f7108da1b3","version":"v9.0.0"},{"repo":"actions/setup-node","sha":"820762786026740c76f36085b0efc47a31fe5020","version":"v7.0.0"},{"repo":"actions/upload-artifact","sha":"043fb46d1a93c77aae656e7c1c64a875d1fc6a0a","version":"v7.0.1"},{"repo":"github/gh-aw-actions/setup","sha":"v0.83.4","version":"v0.83.4"}],"containers":[{"image":"ghcr.io/github/gh-aw-firewall/agent:0.27.42","digest":"sha256:26a8af4e5566485b02f52af59ee03803ae798271a9619d4767e94d07806deb9b","pinned_image":"ghcr.io/github/gh-aw-firewall/agent:0.27.42@sha256:26a8af4e5566485b02f52af59ee03803ae798271a9619d4767e94d07806deb9b"},{"image":"ghcr.io/github/gh-aw-firewall/api-proxy:0.27.42","digest":"sha256:944f2686c9ab9bec338fd14b662461662f77cd12cd0ea8a3e7cb8c0987cd1607","pinned_image":"ghcr.io/github/gh-aw-firewall/api-proxy:0.27.42@sha256:944f2686c9ab9bec338fd14b662461662f77cd12cd0ea8a3e7cb8c0987cd1607"},{"image":"ghcr.io/github/gh-aw-firewall/squid:0.27.42","digest":"sha256:42dfeb649c680a8558cd5423dbc530b653a69413e35ffbe5e71da5d48c94bdf0","pinned_image":"ghcr.io/github/gh-aw-firewall/squid:0.27.42@sha256:42dfeb649c680a8558cd5423dbc530b653a69413e35ffbe5e71da5d48c94bdf0"},{"image":"ghcr.io/github/gh-aw-mcpg:v0.4.6","digest":"sha256:fecabec51bbc41f2ad61076d6bcd9a36ef23b142e672a444e054d37fc29de93c","pinned_image":"ghcr.io/github/gh-aw-mcpg:v0.4.6@sha256:fecabec51bbc41f2ad61076d6bcd9a36ef23b142e672a444e054d37fc29de93c"},{"image":"ghcr.io/github/gh-aw-node","digest":"sha256:a8082161d7dceda14b68f32eb39d0eaa96b825d07f5895b096afab9d9e0c7748","pinned_image":"ghcr.io/github/gh-aw-node@sha256:a8082161d7dceda14b68f32eb39d0eaa96b825d07f5895b096afab9d9e0c7748"},{"image":"ghcr.io/github/github-mcp-server:v1.7.0","digest":"sha256:c491ffdf6f4c85cb5397021bc655edb8ab825c6f5f568e7597d77a1bd7c4d308","pinned_image":"ghcr.io/github/github-mcp-server:v1.7.0@sha256:c491ffdf6f4c85cb5397021bc655edb8ab825c6f5f568e7597d77a1bd7c4d308"}]}
 # This file was automatically generated by gh-aw (v0.83.4). DO NOT EDIT. To debug this workflow, load the skill at https://github.com/github/gh-aw/blob/main/debug.md
 #
@@ -23,7 +23,7 @@
 #
 # For more information: https://github.github.com/gh-aw/introduction/overview/
 #
-# Automatically builds Z3 directly and fixes detected build warnings
+# Compiles Z3 with clang-tidy, analyzes build warnings and errors, and creates PRs with safe fixes
 #
 # Secrets used:
 #   - COPILOT_GITHUB_TOKEN
@@ -51,10 +51,11 @@
 #   - ghcr.io/github/gh-aw-node@sha256:a8082161d7dceda14b68f32eb39d0eaa96b825d07f5895b096afab9d9e0c7748
 #   - ghcr.io/github/github-mcp-server:v1.7.0@sha256:c491ffdf6f4c85cb5397021bc655edb8ab825c6f5f568e7597d77a1bd7c4d308
 
-name: "Build Warning Fixer"
+name: "Clang-Tidy Warning Fixer"
 on:
   schedule:
     - cron: "9 21 * * *"  # Friendly format: daily (scattered)
+  # skip-if-match: is:pr is:open in:title "[clang-tidy]" # Skip-if-match processed as search check in pre-activation job
   workflow_dispatch:
     inputs:
       aw_context:
@@ -68,10 +69,12 @@ permissions: {}
 concurrency:
   group: "gh-aw-${{ github.workflow }}"
 
-run-name: "Build Warning Fixer"
+run-name: "Clang-Tidy Warning Fixer"
 
 jobs:
   activation:
+    needs: pre_activation
+    if: needs.pre_activation.outputs.activated == 'true'
     runs-on: ubuntu-slim
     permissions:
       actions: read
@@ -89,7 +92,6 @@ jobs:
       lockdown_check_failed: ${{ steps.generate_aw_info.outputs.lockdown_check_failed == 'true' }}
       model: ${{ steps.generate_aw_info.outputs.model }}
       oauth_token_check_failed: ${{ steps.check-oauth-tokens.outputs.oauth_token_check_failed == 'true' }}
-      secret_verification_result: ${{ steps.validate-secret.outputs.verification_result }}
       setup-parent-span-id: ${{ steps.setup.outputs.parent-span-id || steps.setup.outputs.span-id }}
       setup-span-id: ${{ steps.setup.outputs.span-id }}
       setup-trace-id: ${{ steps.setup.outputs.trace-id }}
@@ -101,9 +103,11 @@ jobs:
         with:
           destination: ${{ runner.temp }}/gh-aw/actions
           job-name: ${{ github.job }}
+          trace-id: ${{ needs.pre_activation.outputs.setup-trace-id }}
+          parent-span-id: ${{ needs.pre_activation.outputs.setup-parent-span-id || needs.pre_activation.outputs.setup-span-id }}
           safe-output-artifact-client: ${{ env.GH_AW_MAX_DAILY_AI_CREDITS != '' }}
         env:
-          GH_AW_SETUP_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_SETUP_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/build-warning-fixer.lock.yml@${{ github.ref }}
           GH_AW_INFO_VERSION: "1.0.75"
           GH_AW_INFO_AWF_VERSION: "v0.27.42"
@@ -117,7 +121,7 @@ jobs:
           GH_AW_INFO_VERSION: "1.0.75"
           GH_AW_INFO_AGENT_VERSION: "1.0.75"
           GH_AW_INFO_CLI_VERSION: "v0.83.4"
-          GH_AW_INFO_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_INFO_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_INFO_EXPERIMENTAL: "false"
           GH_AW_INFO_SUPPORTS_TOOLS_ALLOWLIST: "true"
           GH_AW_INFO_STAGED: "false"
@@ -163,7 +167,7 @@ jobs:
         if: ${{ env.GH_AW_MAX_DAILY_AI_CREDITS != '' }}
         uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
         env:
-          GH_AW_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_WORKFLOW_ID: "build-warning-fixer"
           GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
           GH_AW_WORKFLOW_DISPATCH_AW_CONTEXT: ${{ github.event.inputs.aw_context || '' }}
@@ -178,11 +182,6 @@ jobs:
             setupGlobals(core, github, context, exec, io, getOctokit);
             const { main } = require('${{ runner.temp }}/gh-aw/actions/check_daily_aic_workflow_guardrail.cjs');
             await main();
-      - name: Validate COPILOT_GITHUB_TOKEN secret
-        id: validate-secret
-        run: bash "${RUNNER_TEMP}/gh-aw/actions/validate_multi_secret.sh" COPILOT_GITHUB_TOKEN 'GitHub Copilot CLI' https://github.github.com/gh-aw/reference/engines/#github-copilot-default
-        env:
-          COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
       - name: Check for OAuth tokens
         id: check-oauth-tokens
         run: bash "${RUNNER_TEMP}/gh-aw/actions/check_oauth_tokens.sh"
@@ -247,6 +246,7 @@ jobs:
           GH_AW_GITHUB_ACTOR: ${{ github.actor }}
           GH_AW_GITHUB_REPOSITORY: ${{ github.repository }}
           GH_AW_GITHUB_RUN_ID: ${{ github.run_id }}
+          GH_AW_GITHUB_WORKFLOW: ${{ github.workflow }}
           GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }}
         # poutine:ignore untrusted_checkout_exec
         run: |
@@ -309,6 +309,9 @@ jobs:
         env:
           GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
           GH_AW_ENGINE_ID: "copilot"
+          GH_AW_GITHUB_REPOSITORY: ${{ github.repository }}
+          GH_AW_GITHUB_WORKFLOW: ${{ github.workflow }}
+          GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }}
         with:
           script: |
             const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs');
@@ -326,8 +329,10 @@ jobs:
           GH_AW_GITHUB_ACTOR: ${{ github.actor }}
           GH_AW_GITHUB_REPOSITORY: ${{ github.repository }}
           GH_AW_GITHUB_RUN_ID: ${{ github.run_id }}
+          GH_AW_GITHUB_WORKFLOW: ${{ github.workflow }}
           GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }}
           GH_AW_MCP_CLI_SERVERS_LIST: "- `github` — run `github --help` to see available tools\n- `safeoutputs` — run `safeoutputs --help` to see available tools"
+          GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_ACTIVATED: ${{ needs.pre_activation.outputs.activated }}
         with:
           script: |
             const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs');
@@ -346,8 +351,10 @@ jobs:
                 GH_AW_GITHUB_ACTOR: process.env.GH_AW_GITHUB_ACTOR,
                 GH_AW_GITHUB_REPOSITORY: process.env.GH_AW_GITHUB_REPOSITORY,
                 GH_AW_GITHUB_RUN_ID: process.env.GH_AW_GITHUB_RUN_ID,
+                GH_AW_GITHUB_WORKFLOW: process.env.GH_AW_GITHUB_WORKFLOW,
                 GH_AW_GITHUB_WORKSPACE: process.env.GH_AW_GITHUB_WORKSPACE,
-                GH_AW_MCP_CLI_SERVERS_LIST: process.env.GH_AW_MCP_CLI_SERVERS_LIST
+                GH_AW_MCP_CLI_SERVERS_LIST: process.env.GH_AW_MCP_CLI_SERVERS_LIST,
+                GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_ACTIVATED: process.env.GH_AW_NEEDS_PRE_ACTIVATION_OUTPUTS_ACTIVATED
               }
             });
       - name: Validate prompt placeholders
@@ -383,7 +390,11 @@ jobs:
     needs: activation
     if: needs.activation.outputs.daily_ai_credits_exceeded != 'true'
     runs-on: ubuntu-latest
-    permissions: read-all
+    permissions:
+      contents: read
+      copilot-requests: write
+      issues: read
+      pull-requests: read
     concurrency:
       group: "gh-aw-copilot-${{ github.workflow }}"
       queue: max
@@ -425,7 +436,7 @@ jobs:
           trace-id: ${{ needs.activation.outputs.setup-trace-id }}
           parent-span-id: ${{ needs.activation.outputs.setup-parent-span-id || needs.activation.outputs.setup-span-id }}
         env:
-          GH_AW_SETUP_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_SETUP_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/build-warning-fixer.lock.yml@${{ github.ref }}
           GH_AW_INFO_VERSION: "1.0.75"
           GH_AW_INFO_AWF_VERSION: "v0.27.42"
@@ -511,15 +522,15 @@ jobs:
           mkdir -p "${RUNNER_TEMP}/gh-aw/safeoutputs"
           mkdir -p /tmp/gh-aw/safeoutputs
           mkdir -p /tmp/gh-aw/mcp-logs/safeoutputs
-          cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_9662473be8d97bf8_EOF'
-          {"create_pull_request":{"if_no_changes":"ignore","max":1,"max_patch_files":100,"max_patch_size":4096,"protect_top_level_dot_folders":true,"protected_files":["package.json","bun.lockb","bunfig.toml","deno.json","deno.jsonc","deno.lock","global.json","NuGet.Config","Directory.Packages.props","mix.exs","mix.lock","go.mod","go.sum","stack.yaml","stack.yaml.lock","pom.xml","build.gradle","build.gradle.kts","settings.gradle","settings.gradle.kts","gradle.properties","package-lock.json","yarn.lock","pnpm-lock.yaml","npm-shrinkwrap.json","requirements.txt","Pipfile","Pipfile.lock","pyproject.toml","setup.py","setup.cfg","Gemfile","Gemfile.lock","uv.lock","CODEOWNERS","DESIGN.md","README.md","CONTRIBUTING.md","CHANGELOG.md","SECURITY.md","CODE_OF_CONDUCT.md","AGENTS.md","CLAUDE.md","GEMINI.md"],"protected_files_policy":"request_review"},"create_report_incomplete_issue":{},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}}
-          GH_AW_SAFE_OUTPUTS_CONFIG_9662473be8d97bf8_EOF
+          cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_7961ea29efc7290e_EOF'
+          {"create_pull_request":{"expires":24,"if_no_changes":"ignore","labels":["code-quality","clang-tidy","automation"],"max":1,"max_patch_files":100,"max_patch_size":4096,"protect_top_level_dot_folders":true,"protected_files":["package.json","bun.lockb","bunfig.toml","deno.json","deno.jsonc","deno.lock","global.json","NuGet.Config","Directory.Packages.props","mix.exs","mix.lock","go.mod","go.sum","stack.yaml","stack.yaml.lock","pom.xml","build.gradle","build.gradle.kts","settings.gradle","settings.gradle.kts","gradle.properties","package-lock.json","yarn.lock","pnpm-lock.yaml","npm-shrinkwrap.json","requirements.txt","Pipfile","Pipfile.lock","pyproject.toml","setup.py","setup.cfg","Gemfile","Gemfile.lock","uv.lock","CODEOWNERS","DESIGN.md","README.md","CONTRIBUTING.md","CHANGELOG.md","SECURITY.md","CODE_OF_CONDUCT.md","AGENTS.md","CLAUDE.md","GEMINI.md"],"protected_files_policy":"request_review","reviewers":["copilot"],"title_prefix":"[clang-tidy] "},"create_report_incomplete_issue":{},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}}
+          GH_AW_SAFE_OUTPUTS_CONFIG_7961ea29efc7290e_EOF
       - name: Generate Safe Outputs Tools
         env:
           GH_AW_TOOLS_META_JSON: |
             {
               "description_suffixes": {
-                "create_pull_request": " CONSTRAINTS: Maximum 1 pull request(s) can be created."
+                "create_pull_request": " CONSTRAINTS: Maximum 1 pull request(s) can be created. Title will be prefixed with \"[clang-tidy] \". Labels [\"code-quality\" \"clang-tidy\" \"automation\"] will be automatically added. Reviewers [\"copilot\"] will be assigned."
               },
               "repo_params": {},
               "dynamic_tools": []
@@ -770,7 +781,7 @@ jobs:
       - name: Execute GitHub Copilot CLI
         id: agentic_execution
         # Copilot CLI tool arguments (sorted):
-        timeout-minutes: 60
+        timeout-minutes: 90
         run: |
           set -o pipefail
           printf '%s' "$(date +%s%3N)" > /tmp/gh-aw/agent_cli_start_ms.txt
@@ -809,7 +820,7 @@ jobs:
           AWF_REFLECT_ENABLED: 1
           COPILOT_AGENT_RUNNER_TYPE: STANDALONE
           COPILOT_DUMMY_BYOK: dummy-byok-key-for-offline-mode
-          COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
+          COPILOT_GITHUB_TOKEN: ${{ github.token }}
           COPILOT_MODEL: ${{ vars.GH_AW_MODEL_AGENT_COPILOT || vars.GH_AW_DEFAULT_MODEL_COPILOT || 'claude-sonnet-4.6' }}
           GH_AW_LLM_PROVIDER: github
           GH_AW_MAX_AI_CREDITS: ${{ vars.GH_AW_DEFAULT_MAX_AI_CREDITS || '1000' }}
@@ -817,7 +828,7 @@ jobs:
           GH_AW_PHASE: agent
           GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
           GH_AW_SAFE_OUTPUTS: ${{ steps.set-runtime-paths.outputs.GH_AW_SAFE_OUTPUTS }}
-          GH_AW_TIMEOUT_MINUTES: 60
+          GH_AW_TIMEOUT_MINUTES: 90
           GH_AW_VERSION: v0.83.4
           GITHUB_API_URL: ${{ github.api_url }}
           GITHUB_AW: true
@@ -833,6 +844,7 @@ jobs:
           GIT_COMMITTER_EMAIL: github-actions[bot]@users.noreply.github.com
           GIT_COMMITTER_NAME: github-actions[bot]
           RUNNER_TEMP: ${{ runner.temp }}
+          S2STOKENS: true
           TRACEPARENT: ${{ env.GITHUB_AW_OTEL_TRACE_ID != '' && env.GITHUB_AW_OTEL_PARENT_SPAN_ID != '' && format('00-{0}-{1}-01', env.GITHUB_AW_OTEL_TRACE_ID, env.GITHUB_AW_OTEL_PARENT_SPAN_ID) || '' }}
       - name: Detect agent errors
         if: always()
@@ -868,8 +880,7 @@ jobs:
             const { main } = require('${{ runner.temp }}/gh-aw/actions/redact_secrets.cjs');
             await main();
         env:
-          GH_AW_SECRET_NAMES: 'COPILOT_GITHUB_TOKEN,GH_AW_GITHUB_MCP_SERVER_TOKEN,GH_AW_GITHUB_TOKEN,GITHUB_TOKEN'
-          SECRET_COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
+          GH_AW_SECRET_NAMES: 'GH_AW_GITHUB_MCP_SERVER_TOKEN,GH_AW_GITHUB_TOKEN,GITHUB_TOKEN'
           SECRET_GH_AW_GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN }}
           SECRET_GH_AW_GITHUB_TOKEN: ${{ secrets.GH_AW_GITHUB_TOKEN }}
           SECRET_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
@@ -987,7 +998,7 @@ jobs:
     if: >
       always() && (needs.agent.result != 'skipped' || needs.activation.outputs.lockdown_check_failed == 'true' ||
       needs.activation.outputs.oauth_token_check_failed == 'true' || needs.activation.outputs.stale_lock_file_failed == 'true' ||
-      needs.activation.outputs.secret_verification_result == 'failed' || needs.activation.outputs.daily_ai_credits_exceeded == 'true')
+      needs.activation.outputs.daily_ai_credits_exceeded == 'true')
     runs-on: ubuntu-slim
     permissions:
       contents: write
@@ -1014,7 +1025,7 @@ jobs:
           trace-id: ${{ needs.activation.outputs.setup-trace-id }}
           parent-span-id: ${{ needs.activation.outputs.setup-parent-span-id || needs.activation.outputs.setup-span-id }}
         env:
-          GH_AW_SETUP_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_SETUP_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/build-warning-fixer.lock.yml@${{ github.ref }}
           GH_AW_INFO_VERSION: "1.0.75"
           GH_AW_INFO_AWF_VERSION: "v0.27.42"
@@ -1131,8 +1142,9 @@ jobs:
         env:
           GH_AW_AGENT_OUTPUT: ${{ steps.setup-agent-output-env.outputs.GH_AW_AGENT_OUTPUT }}
           GH_AW_NOOP_MAX: "1"
-          GH_AW_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/build-warning-fixer.md"
+          GH_AW_TRACKER_ID: "clang-tidy-warning-fixer"
           GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
           GH_AW_AGENT_CONCLUSION: ${{ needs.agent.result }}
           GH_AW_NOOP_REPORT_AS_ISSUE: "false"
@@ -1152,8 +1164,9 @@ jobs:
         uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
         env:
           GH_AW_AGENT_OUTPUT: ${{ steps.setup-agent-output-env.outputs.GH_AW_AGENT_OUTPUT }}
-          GH_AW_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/build-warning-fixer.md"
+          GH_AW_TRACKER_ID: "clang-tidy-warning-fixer"
           GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
           GH_AW_DETECTION_CONCLUSION: ${{ needs.detection.outputs.detection_conclusion }}
           GH_AW_DETECTION_REASON: ${{ needs.detection.outputs.detection_reason }}
@@ -1171,8 +1184,9 @@ jobs:
           GH_AW_AGENT_OUTPUT: ${{ steps.setup-agent-output-env.outputs.GH_AW_AGENT_OUTPUT }}
           GH_AW_MISSING_TOOL_CREATE_ISSUE: "true"
           GH_AW_MISSING_TOOL_TITLE_PREFIX: "[missing tool]"
-          GH_AW_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/build-warning-fixer.md"
+          GH_AW_TRACKER_ID: "clang-tidy-warning-fixer"
         with:
           github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
           script: |
@@ -1186,8 +1200,9 @@ jobs:
         env:
           GH_AW_AGENT_OUTPUT: ${{ steps.setup-agent-output-env.outputs.GH_AW_AGENT_OUTPUT }}
           GH_AW_REPORT_INCOMPLETE_CREATE_ISSUE: "true"
-          GH_AW_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/build-warning-fixer.md"
+          GH_AW_TRACKER_ID: "clang-tidy-warning-fixer"
         with:
           github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
           script: |
@@ -1201,15 +1216,14 @@ jobs:
         uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
         env:
           GH_AW_AGENT_OUTPUT: ${{ steps.setup-agent-output-env.outputs.GH_AW_AGENT_OUTPUT }}
-          GH_AW_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/build-warning-fixer.md"
+          GH_AW_TRACKER_ID: "clang-tidy-warning-fixer"
           GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
           GH_AW_AGENT_CONCLUSION: ${{ needs.agent.result }}
           GH_AW_WORKFLOW_ID: "build-warning-fixer"
           GH_AW_ACTION_FAILURE_ISSUE_EXPIRES_HOURS: "168"
           GH_AW_ENGINE_ID: "copilot"
-          GH_AW_SECRET_VERIFICATION_RESULT: ${{ needs.activation.outputs.secret_verification_result }}
-          GH_AW_ENGINE_SECRET_FAILURE_MESSAGE: "**Alternative**: If your organization has a Copilot subscription, you can avoid the need for a personal access token by adding a top-level `permissions` block to your workflow file. This enables Copilot inference through the org using the built-in GitHub Actions token.\n\n```yaml\npermissions:\n  copilot-requests: write\n```\n\nSee: https://github.github.com/gh-aw/reference/engines/#github-copilot-default"
           GH_AW_CHECKOUT_PR_SUCCESS: ${{ needs.agent.outputs.checkout_pr_success }}
           GH_AW_EFFECTIVE_TOKENS: ${{ needs.agent.outputs.effective_tokens || '' }}
           GH_AW_AI_CREDITS_RATE_LIMIT_ERROR: ${{ needs.agent.outputs.ai_credits_rate_limit_error || 'false' }}
@@ -1235,7 +1249,7 @@ jobs:
           GH_AW_FAILURE_REPORT_AS_ISSUE: "false"
           GH_AW_MISSING_TOOL_REPORT_AS_FAILURE: "true"
           GH_AW_MISSING_DATA_REPORT_AS_FAILURE: "true"
-          GH_AW_TIMEOUT_MINUTES: "60"
+          GH_AW_TIMEOUT_MINUTES: "90"
         with:
           github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
           script: |
@@ -1252,6 +1266,7 @@ jobs:
     runs-on: ubuntu-latest
     permissions:
       contents: read
+      copilot-requests: write
     env:
       GH_AW_RUNTIME_FEATURES: ${{ vars.GH_AW_RUNTIME_FEATURES }}
     outputs:
@@ -1269,7 +1284,7 @@ jobs:
           trace-id: ${{ needs.activation.outputs.setup-trace-id }}
           parent-span-id: ${{ needs.activation.outputs.setup-parent-span-id || needs.activation.outputs.setup-span-id }}
         env:
-          GH_AW_SETUP_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_SETUP_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/build-warning-fixer.lock.yml@${{ github.ref }}
           GH_AW_INFO_VERSION: "1.0.75"
           GH_AW_INFO_AWF_VERSION: "v0.27.42"
@@ -1342,8 +1357,8 @@ jobs:
         if: always() && steps.detection_guard.outputs.run_detection == 'true'
         uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
         env:
-          WORKFLOW_NAME: "Build Warning Fixer"
-          WORKFLOW_DESCRIPTION: "Automatically builds Z3 directly and fixes detected build warnings"
+          WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
+          WORKFLOW_DESCRIPTION: "Compiles Z3 with clang-tidy, analyzes build warnings and errors, and creates PRs with safe fixes"
           HAS_PATCH: ${{ needs.agent.outputs.has_patch }}
         with:
           script: |
@@ -1412,7 +1427,7 @@ jobs:
           AWF_REFLECT_ENABLED: 1
           COPILOT_AGENT_RUNNER_TYPE: STANDALONE
           COPILOT_DUMMY_BYOK: dummy-byok-key-for-offline-mode
-          COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
+          COPILOT_GITHUB_TOKEN: ${{ github.token }}
           COPILOT_MODEL: ${{ vars.GH_AW_MODEL_DETECTION_COPILOT || vars.GH_AW_DEFAULT_MODEL_COPILOT || 'claude-sonnet-4.6' }}
           GH_AW_LLM_PROVIDER: github
           GH_AW_MAX_AI_CREDITS: ${{ vars.GH_AW_DEFAULT_DETECTION_MAX_AI_CREDITS || '400' }}
@@ -1434,6 +1449,7 @@ jobs:
           GIT_COMMITTER_EMAIL: github-actions[bot]@users.noreply.github.com
           GIT_COMMITTER_NAME: github-actions[bot]
           RUNNER_TEMP: ${{ runner.temp }}
+          S2STOKENS: true
           TRACEPARENT: ${{ env.GITHUB_AW_OTEL_TRACE_ID != '' && env.GITHUB_AW_OTEL_PARENT_SPAN_ID != '' && format('00-{0}-{1}-01', env.GITHUB_AW_OTEL_TRACE_ID, env.GITHUB_AW_OTEL_PARENT_SPAN_ID) || '' }}
       - name: Parse threat detection token usage for step summary
         id: parse_detection_token_usage
@@ -1488,6 +1504,55 @@ jobs:
               }
             }
 
+  pre_activation:
+    runs-on: ubuntu-slim
+    env:
+      GH_AW_RUNTIME_FEATURES: ${{ vars.GH_AW_RUNTIME_FEATURES }}
+    outputs:
+      activated: ${{ steps.check_membership.outputs.is_team_member == 'true' && steps.check_skip_if_match.outputs.skip_check_ok == 'true' }}
+      matched_command: ''
+      setup-parent-span-id: ${{ steps.setup.outputs.parent-span-id || steps.setup.outputs.span-id }}
+      setup-span-id: ${{ steps.setup.outputs.span-id }}
+      setup-trace-id: ${{ steps.setup.outputs.trace-id }}
+    steps:
+      - name: Setup Scripts
+        id: setup
+        uses: github/gh-aw-actions/setup@v0.83.4
+        with:
+          destination: ${{ runner.temp }}/gh-aw/actions
+          job-name: ${{ github.job }}
+        env:
+          GH_AW_SETUP_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
+          GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/build-warning-fixer.lock.yml@${{ github.ref }}
+          GH_AW_INFO_VERSION: "1.0.75"
+          GH_AW_INFO_AWF_VERSION: "v0.27.42"
+          GH_AW_INFO_ENGINE_ID: "copilot"
+      - name: Check team membership for workflow
+        id: check_membership
+        uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
+        env:
+          GH_AW_REQUIRED_ROLES: "admin,maintainer,write"
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs');
+            setupGlobals(core, github, context, exec, io, getOctokit);
+            const { main } = require('${{ runner.temp }}/gh-aw/actions/check_membership.cjs');
+            await main();
+      - name: Check skip-if-match query
+        id: check_skip_if_match
+        uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
+        env:
+          GH_AW_SKIP_QUERY: "is:pr is:open in:title \"[clang-tidy]\""
+          GH_AW_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
+          GH_AW_SKIP_MAX_MATCHES: "1"
+        with:
+          script: |
+            const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs');
+            setupGlobals(core, github, context, exec, io, getOctokit);
+            const { main } = require('${{ runner.temp }}/gh-aw/actions/check_skip_if_match.cjs');
+            await main();
+
   safe_outputs:
     needs:
       - activation
@@ -1513,8 +1578,9 @@ jobs:
       GH_AW_ENGINE_VERSION: "1.0.75"
       GH_AW_RUNTIME_FEATURES: ${{ vars.GH_AW_RUNTIME_FEATURES }}
       GH_AW_THREAT_DETECTION_AIC: ${{ needs.detection.outputs.aic }}
+      GH_AW_TRACKER_ID: "clang-tidy-warning-fixer"
       GH_AW_WORKFLOW_ID: "build-warning-fixer"
-      GH_AW_WORKFLOW_NAME: "Build Warning Fixer"
+      GH_AW_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
       GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/build-warning-fixer.md"
     outputs:
       code_push_failure_count: ${{ steps.process_safe_outputs.outputs.code_push_failure_count }}
@@ -1535,7 +1601,7 @@ jobs:
           trace-id: ${{ needs.activation.outputs.setup-trace-id }}
           parent-span-id: ${{ needs.activation.outputs.setup-parent-span-id || needs.activation.outputs.setup-span-id }}
         env:
-          GH_AW_SETUP_WORKFLOW_NAME: "Build Warning Fixer"
+          GH_AW_SETUP_WORKFLOW_NAME: "Clang-Tidy Warning Fixer"
           GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/build-warning-fixer.lock.yml@${{ github.ref }}
           GH_AW_INFO_VERSION: "1.0.75"
           GH_AW_INFO_AWF_VERSION: "v0.27.42"
@@ -1591,7 +1657,7 @@ jobs:
           GH_AW_ALLOWED_DOMAINS: "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com,www.googleapis.com"
           GITHUB_SERVER_URL: ${{ github.server_url }}
           GITHUB_API_URL: ${{ github.api_url }}
-          GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_pull_request\":{\"if_no_changes\":\"ignore\",\"max\":1,\"max_patch_files\":100,\"max_patch_size\":4096,\"protect_top_level_dot_folders\":true,\"protected_files\":[\"package.json\",\"bun.lockb\",\"bunfig.toml\",\"deno.json\",\"deno.jsonc\",\"deno.lock\",\"global.json\",\"NuGet.Config\",\"Directory.Packages.props\",\"mix.exs\",\"mix.lock\",\"go.mod\",\"go.sum\",\"stack.yaml\",\"stack.yaml.lock\",\"pom.xml\",\"build.gradle\",\"build.gradle.kts\",\"settings.gradle\",\"settings.gradle.kts\",\"gradle.properties\",\"package-lock.json\",\"yarn.lock\",\"pnpm-lock.yaml\",\"npm-shrinkwrap.json\",\"requirements.txt\",\"Pipfile\",\"Pipfile.lock\",\"pyproject.toml\",\"setup.py\",\"setup.cfg\",\"Gemfile\",\"Gemfile.lock\",\"uv.lock\",\"CODEOWNERS\",\"DESIGN.md\",\"README.md\",\"CONTRIBUTING.md\",\"CHANGELOG.md\",\"SECURITY.md\",\"CODE_OF_CONDUCT.md\",\"AGENTS.md\",\"CLAUDE.md\",\"GEMINI.md\"],\"protected_files_policy\":\"request_review\"},\"create_report_incomplete_issue\":{},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}"
+          GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_pull_request\":{\"expires\":24,\"if_no_changes\":\"ignore\",\"labels\":[\"code-quality\",\"clang-tidy\",\"automation\"],\"max\":1,\"max_patch_files\":100,\"max_patch_size\":4096,\"protect_top_level_dot_folders\":true,\"protected_files\":[\"package.json\",\"bun.lockb\",\"bunfig.toml\",\"deno.json\",\"deno.jsonc\",\"deno.lock\",\"global.json\",\"NuGet.Config\",\"Directory.Packages.props\",\"mix.exs\",\"mix.lock\",\"go.mod\",\"go.sum\",\"stack.yaml\",\"stack.yaml.lock\",\"pom.xml\",\"build.gradle\",\"build.gradle.kts\",\"settings.gradle\",\"settings.gradle.kts\",\"gradle.properties\",\"package-lock.json\",\"yarn.lock\",\"pnpm-lock.yaml\",\"npm-shrinkwrap.json\",\"requirements.txt\",\"Pipfile\",\"Pipfile.lock\",\"pyproject.toml\",\"setup.py\",\"setup.cfg\",\"Gemfile\",\"Gemfile.lock\",\"uv.lock\",\"CODEOWNERS\",\"DESIGN.md\",\"README.md\",\"CONTRIBUTING.md\",\"CHANGELOG.md\",\"SECURITY.md\",\"CODE_OF_CONDUCT.md\",\"AGENTS.md\",\"CLAUDE.md\",\"GEMINI.md\"],\"protected_files_policy\":\"request_review\",\"reviewers\":[\"copilot\"],\"title_prefix\":\"[clang-tidy] \"},\"create_report_incomplete_issue\":{},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}"
           GH_AW_CI_TRIGGER_TOKEN: ${{ secrets.GH_AW_CI_TRIGGER_TOKEN }}
         with:
           github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
diff --git a/.github/workflows/build-warning-fixer.md b/.github/workflows/build-warning-fixer.md
index 12aa9841bf..a269821609 100644
--- a/.github/workflows/build-warning-fixer.md
+++ b/.github/workflows/build-warning-fixer.md
@@ -1,146 +1,166 @@
 ---
-description: Automatically builds Z3 directly and fixes detected build warnings
+name: Clang-Tidy Warning Fixer
+description: Compiles Z3 with clang-tidy, analyzes build warnings and errors, and creates PRs with safe fixes
 on:
   schedule: daily
   workflow_dispatch:
-permissions: read-all
-tools:
-  edit:
-  bash: true
+  skip-if-match: 'is:pr is:open in:title "[clang-tidy]"'
+permissions:
+  contents: read
+  issues: read
+  pull-requests: read
+  copilot-requests: write
+tracker-id: clang-tidy-warning-fixer
 safe-outputs:
   report-failure-as-issue: false
   create-pull-request:
+    title-prefix: "[clang-tidy] "
+    labels: [code-quality, clang-tidy, automation]
+    reviewers: [copilot]
+    expires: 1d
     if-no-changes: ignore
   missing-tool:
     create-issue: true
   noop:
     report-as-issue: false
-timeout-minutes: 60
+network: defaults
+tools:
+  github:
+    toolsets: [default]
+  bash: [":*"]
+timeout-minutes: 90
+strict: true
 ---
 
-# Build Warning Fixer
+# Clang-Tidy Warning Fixer
 
-You are an AI agent that automatically detects and fixes build warnings in the Z3 theorem prover codebase.
+You are an AI agent that compiles Z3 with clang-tidy, reviews the resulting warnings and errors, and creates a pull request with conservative fixes when you can do so safely.
+
+## Current Context
+
+- **Repository**: ${{ github.repository }}
+- **Workflow**: ${{ github.workflow }}
+- **Workspace**: ${{ github.workspace }}
 
 ## Your Task
 
-1. **Pick a random build workflow and build Z3 directly**
-   
-   Available build workflows that you can randomly choose from:
-   - `wip.yml` - Ubuntu CMake Debug build (simple, good default choice)
-   - `cross-build.yml` - Cross-compilation builds (aarch64, riscv64, powerpc64)
-   - `coverage.yml` - Code coverage build with Clang
-   
-   **Steps to build Z3 directly:**
-   
-   a. **Pick ONE workflow randomly** from the list above. Use bash to generate a random choice if needed.
-   
-   b. **Read the workflow file** to understand its build configuration:
-      - Use `view` to read the `.github/workflows/<workflow-name>.yml` file
-      - Identify the build steps, cmake flags, compiler settings, and environment variables
-      - Note the runner type (ubuntu-latest, windows-latest, etc.)
-   
-   c. **Execute the build directly** using bash:
-      - Run the same cmake configuration commands from the workflow
-      - Capture the full build output including warnings
-      - Use `2>&1` to capture both stdout and stderr
-      - Save output to a log file for analysis
-   
-   Example for wip.yml workflow:
-   ```bash
-   # Configure
-   cmake -B build -DCMAKE_BUILD_TYPE=Debug 2>&1 | tee build-config.log
-   
-   # Build and capture output
-   cmake --build build --config Debug 2>&1 | tee build-output.log
-   ```
-   
-   Example for cross-build.yml workflow (pick one arch):
-   ```bash
-   # Pick one architecture randomly
-   ARCH=aarch64  # or riscv64, or powerpc64
-   
-   # Configure
-   mkdir build && cd build
-   cmake -DCMAKE_CXX_COMPILER=${ARCH}-linux-gnu-g++-11 ../ 2>&1 | tee ../build-config.log
-   
-   # Build and capture output
-   make -j$(nproc) 2>&1 | tee ../build-output.log
-   ```
-   
-   d. **Install any necessary dependencies** before building:
-      - For cross-build: `apt update && apt install -y ninja-build cmake python3 g++-11-aarch64-linux-gnu` (or other arch)
-      - For coverage: `apt-get install -y gcovr ninja-build llvm clang`
+### 1. Build Z3 with clang-tidy enabled
 
-2. **Extract compiler warnings** from the direct build output:
-   - Analyze the build-output.log file you created
-   - Use `grep` or `bash` to search for warning patterns
-   - Look for C++ compiler warnings (gcc, clang, MSVC patterns)
-   - Common warning patterns:
-     - `-Wunused-variable`, `-Wunused-parameter`
-     - `-Wsign-compare`, `-Wparentheses`
-     - `-Wdeprecated-declarations`
-     - `-Wformat`, `-Wformat-security`
-     - MSVC warnings like `C4244`, `C4267`, `C4100`
-   - Focus on warnings that appear frequently or are straightforward to fix
+Use the repository's CMake + Ninja workflow and build Z3 directly with Clang.
 
-3. **Analyze the warnings**:
-   - Identify the source files and line numbers
-   - Determine the root cause of each warning
-   - Prioritize warnings that:
-     - Are easy to fix automatically (unused variables, sign mismatches, etc.)
-     - Appear in multiple build configurations
-     - Don't require deep semantic understanding
+1. Install the required tools:
 
-4. **Create fixes**:
-   - Use `view`, `grep`, and `glob` to locate the problematic code
-   - Use `edit` to apply minimal, surgical fixes
-   - Common fix patterns:
-     - Remove or comment out unused variables
-     - Add explicit casts for sign/type mismatches (with care)
-     - Add `[[maybe_unused]]` attributes for intentionally unused parameters
-     - Fix deprecated API usage
-   - **NEVER** make changes that could alter program behavior
-   - **ONLY** fix warnings you're confident about
+```bash
+sudo apt-get update -y
+sudo apt-get install -y clang clang-tidy cmake ninja-build python3
+clang --version
+clang-tidy --version
+ninja --version
+```
 
-5. **Validate the fixes** (if possible):
-   - Use `bash` to run quick compilation checks on modified files
-   - Use `git diff` to review changes before committing
+2. Start from a clean build directory and configure with clang/clang++:
 
-6. **Create a pull request** with your fixes:
-   - Use the `create-pull-request` safe output
-   - Title: "Fix build warnings detected in direct build"
-   - Body should include:
-     - Which workflow configuration was used for the build
-     - List of warnings fixed
-     - Explanation of each change
-     - Note that this is an automated fix requiring human review
+```bash
+rm -rf build
+CC=clang CXX=clang++ cmake -GNinja -S . -B build \
+  -DCMAKE_BUILD_TYPE=Debug \
+  -DCMAKE_EXPORT_COMPILE_COMMANDS=ON \
+  -DCMAKE_CXX_CLANG_TIDY=clang-tidy \
+  2>&1 | tee /tmp/gh-aw/agent/clang-tidy-configure.log
+```
+
+3. Build the main Z3 shell and unit test binary while capturing logs:
+
+```bash
+cmake --build build --target shell test-z3 -k 0 2>&1 | tee /tmp/gh-aw/agent/clang-tidy-build.log
+```
+
+4. If configuration fails, inspect `/tmp/gh-aw/agent/clang-tidy-configure.log` and call `noop` with a clear summary unless you can make an obvious, local, semantics-preserving fix.
+
+### 2. Extract actionable diagnostics
+
+Analyze `/tmp/gh-aw/agent/clang-tidy-build.log` and focus on diagnostics that clang-tidy or clang emitted during this workflow run.
+
+Use commands like:
+
+```bash
+grep -nE 'warning:|error:|clang-tidy' /tmp/gh-aw/agent/clang-tidy-build.log | head -200
+```
+
+Classify findings into:
+- **clang-tidy warnings**
+- **compiler warnings**
+- **compiler or build errors**
+
+Prioritize findings that are:
+- localized to one file
+- straightforward to fix safely
+- unlikely to change behavior
+- validated by rebuilding
+
+Skip findings that require design changes, broad refactors, or uncertain semantic changes.
+
+### 3. Investigate the affected code
+
+For each high-confidence finding:
+
+1. Locate the file and exact lines.
+2. Read the surrounding code.
+3. Confirm the warning is real and not already fixed.
+4. Prefer the smallest possible change.
+
+Examples of usually safe fixes:
+- removing dead or unused locals
+- adding `override` where the class already overrides a virtual method
+- adding `[[maybe_unused]]` for intentionally unused parameters or variables
+- replacing obvious null literal usage with `nullptr`
+- applying other trivial clang-tidy modernizations that do not alter behavior
+
+Do **not** change behavior, APIs, ownership, solver logic, or performance-sensitive code unless the fix is obviously semantics-preserving.
+
+### 4. Apply fixes conservatively
+
+When you are confident, edit the relevant files and keep the patch minimal.
+
+Rules:
+- fix only warnings you fully understand
+- do not batch unrelated cleanups
+- preserve formatting and local style
+- if a finding is uncertain, skip it instead of guessing
+
+### 5. Rebuild and confirm the fixes
+
+After making changes, rerun the same configure/build sequence if needed and always rerun at least:
+
+```bash
+cmake --build build --target shell test-z3 -k 0 2>&1 | tee /tmp/gh-aw/agent/clang-tidy-build-after.log
+./build/test-z3 /a
+```
+
+If the rebuilt logs still contain actionable warnings, you may fix another small set if you remain confident. Otherwise stop.
+
+### 6. Create the pull request
+
+If you made safe fixes, create a pull request using `create-pull-request`.
+
+Use a title describing the warnings fixed, for example:
+- `Fix clang-tidy warnings in parser code`
+- `Fix clang-tidy override and unused warnings`
+
+The PR body should include:
+- that the workflow compiled Z3 with clang-tidy
+- the build command that was used
+- the files changed
+- the warnings or errors fixed
+- confirmation that you rebuilt and ran `./build/test-z3 /a`
+- a brief note for any remaining warnings you intentionally skipped
+
+If there are no safe fixes to make, call `noop` with a short summary of what you built and what you found.
 
 ## Guidelines
 
-- **Be conservative**: Only fix warnings you're 100% certain about
-- **Minimal changes**: Don't refactor or improve code beyond fixing the warning
-- **Preserve semantics**: Never change program behavior
-- **Document clearly**: Explain each fix in the PR description
-- **Skip if uncertain**: If a warning requires deep analysis, note it in the PR but don't attempt to fix it
-- **Focus on low-hanging fruit**: Unused variables, sign mismatches, simple deprecations
-- **Check multiple builds**: Cross-reference warnings across different platforms if possible
-- **Respect existing style**: Match the coding conventions in each file
-
-## Examples of Safe Fixes
-
-✅ **Safe**:
-- Removing truly unused local variables
-- Adding `(void)param;` or `[[maybe_unused]]` for intentionally unused parameters
-- Adding explicit casts like `static_cast<unsigned>(value)` for sign conversions (when safe)
-- Fixing obvious typos in format strings
-
-❌ **Unsafe** (skip these):
-- Warnings about potential null pointer dereferences (needs careful analysis)
-- Complex type conversion warnings (might hide bugs)
-- Warnings in performance-critical code (might affect benchmarks)
-- Warnings that might indicate actual bugs (file an issue instead)
-
-## Output
-
-If you find and fix warnings, create a PR. If no warnings are found or all warnings are too complex to auto-fix, exit gracefully without creating a PR.
\ No newline at end of file
+- Be conservative and high-confidence only.
+- Prefer no PR over a risky PR.
+- Keep fixes surgical and easy to review.
+- Validate every change by rebuilding.
+- Focus on diagnostics produced by this workflow run, not on unrelated code quality ideas.