diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml
new file mode 100644
index 000000000..64a9ee89b
--- /dev/null
+++ b/.github/workflows/fstar-master-build.yml
@@ -0,0 +1,185 @@
+name: Build FStar master with Z3 master
+
+on:
+  schedule:
+    - cron: "9 4 * * *"
+  workflow_dispatch:
+    inputs:
+      z3_ref:
+        description: Z3 ref to checkout and build
+        required: false
+        default: master
+      z3_cmake_args:
+        description: Extra CMake arguments for Z3 build
+        required: false
+        default: ""
+      z3_runtime_args:
+        description: "Extra Z3 runtime args (example: smt.ho_matching=true)"
+        required: false
+        default: "smt.ho_matching=true"
+      fstar_ref:
+        description: FStar ref to checkout and build
+        required: false
+        default: master
+      fstar_opam_switch:
+        description: OCaml switch for FStar build
+        required: false
+        default: "4.14.2"
+      fstar_otherflags:
+        description: "Extra FStar OTHERFLAGS (example: --smt.ho_matching true)"
+        required: false
+        default: "--smt.ho_matching true"
+      discussion_category:
+        description: Discussion category name
+        required: false
+        default: "Agentic Workflows"
+
+permissions:
+  contents: read
+  discussions: write
+
+concurrency:
+  group: ${{ github.workflow }}
+  cancel-in-progress: false
+
+jobs:
+  build-and-report:
+    runs-on: ubuntu-latest
+    timeout-minutes: 180
+    env:
+      Z3_REF: ${{ github.event.inputs.z3_ref || 'master' }}
+      Z3_CMAKE_ARGS: ${{ github.event.inputs.z3_cmake_args || '' }}
+      Z3_RUNTIME_ARGS: ${{ github.event.inputs.z3_runtime_args || 'smt.ho_matching=true' }}
+      FSTAR_REF: ${{ github.event.inputs.fstar_ref || 'master' }}
+      FSTAR_OPAM_SWITCH: ${{ github.event.inputs.fstar_opam_switch || '4.14.2' }}
+      FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '--smt.ho_matching true' }}
+      DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }}
+    steps:
+      - name: Checkout Z3
+        uses: actions/checkout@v6.0.3
+        with:
+          ref: ${{ env.Z3_REF }}
+          fetch-depth: 1
+
+      - name: Install dependencies
+        run: |
+          set -euo pipefail
+          sudo apt-get update -y
+          sudo apt-get install -y cmake ninja-build python3 git curl unzip opam m4 pkg-config libgmp-dev
+
+      - name: Build Z3
+        run: |
+          set -euo pipefail
+          mkdir -p /tmp/gh-aw/agent
+          cmake -S . -B build/release -G Ninja -DCMAKE_BUILD_TYPE=Release $Z3_CMAKE_ARGS
+          ninja -C build/release z3
+          ./build/release/z3 --version | tee /tmp/gh-aw/agent/z3-version.txt
+          printf '(check-sat)\n' | ./build/release/z3 $Z3_RUNTIME_ARGS -in | tee /tmp/gh-aw/agent/z3-runtime-check.txt
+
+      - name: Prepare Z3 aliases for FStar
+        run: |
+          set -euo pipefail
+          mkdir -p /tmp/gh-aw/agent/z3-bin
+          ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3
+          ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3-4.8.5
+          ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3-4.13.3
+          /tmp/gh-aw/agent/z3-bin/z3 --version
+
+      - name: Build FStar
+        run: |
+          set -euo pipefail
+          rm -rf /tmp/gh-aw/agent/FStar
+          git clone --depth=1 --branch "$FSTAR_REF" https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar
+          cd /tmp/gh-aw/agent/FStar
+          echo "FStar commit: $(git rev-parse HEAD)" | tee /tmp/gh-aw/agent/fstar-commit.txt
+
+          opam init --disable-sandboxing --yes
+          opam switch create "$FSTAR_OPAM_SWITCH" --yes || opam switch "$FSTAR_OPAM_SWITCH"
+          eval "$(opam env --switch="$FSTAR_OPAM_SWITCH")"
+          opam install --deps-only . --yes
+
+          Z3_VERSION="$(sed -E -n 's/^Z3 version ([0-9]+\.[0-9]+\.[0-9]+).*/\1/p' /tmp/gh-aw/agent/z3-version.txt | head -1)"
+          test -n "$Z3_VERSION" || { echo "Error: Failed to extract Z3 version from /tmp/gh-aw/agent/z3-version.txt (expected: 'Z3 version X.Y.Z')"; cat /tmp/gh-aw/agent/z3-version.txt || true; exit 1; }
+
+          PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="--z3version $Z3_VERSION $FSTAR_OTHERFLAGS" make -j"$(nproc)"
+          test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe || { echo "Error: FStar binary not found or not executable at /tmp/gh-aw/agent/FStar/out/bin/fstar.exe"; exit 1; }
+          /tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt
+
+      - name: Create discussion summary
+        uses: actions/github-script@v9
+        env:
+          RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+        with:
+          script: |
+            const fs = require('fs');
+
+            const z3VersionText = fs.readFileSync('/tmp/gh-aw/agent/z3-version.txt', 'utf8').trim();
+            const fstarVersionFile = fs.readFileSync('/tmp/gh-aw/agent/fstar-version.txt', 'utf8').trim();
+            const fstarVersionText = fstarVersionFile ? fstarVersionFile.split('\n')[0] : 'unknown';
+            const fstarCommitLine = fs.readFileSync('/tmp/gh-aw/agent/fstar-commit.txt', 'utf8').trim();
+            const fstarCommit = fstarCommitLine.replace(/^FStar commit:\s*/, '');
+            const date = new Date().toISOString().slice(0, 10);
+
+            const owner = context.repo.owner;
+            const repo = context.repo.repo;
+            const categoryName = process.env.DISCUSSION_CATEGORY;
+
+            const categoryQuery = await github.graphql(
+              `query($owner:String!, $repo:String!) {
+                repository(owner:$owner, name:$repo) {
+                  id
+                  discussionCategories(first:50) {
+                    nodes { id name }
+                  }
+                }
+              }`,
+              { owner, repo }
+            );
+
+            const categories = categoryQuery.repository.discussionCategories.nodes || [];
+            const normalized = categoryName.trim().toLowerCase();
+            const category = categories.find(c => c.name.toLowerCase() === normalized);
+            if (!category) {
+              throw new Error(`Discussion category '${categoryName}' not found`);
+            }
+
+            const body = [
+              `### Build status`,
+              `- ✅ Z3 build completed`,
+              `- ✅ FStar build completed`,
+              ``,
+              `### Inputs used`,
+              `- z3_ref: \`${process.env.Z3_REF}\``,
+              `- z3_cmake_args: \`${process.env.Z3_CMAKE_ARGS}\``,
+              `- z3_runtime_args: \`${process.env.Z3_RUNTIME_ARGS}\``,
+              `- fstar_ref: \`${process.env.FSTAR_REF}\``,
+              `- fstar_opam_switch: \`${process.env.FSTAR_OPAM_SWITCH}\``,
+              `- fstar_otherflags: \`${process.env.FSTAR_OTHERFLAGS}\``,
+              ``,
+              `### Produced versions`,
+              `- Z3: \`${z3VersionText}\``,
+              `- FStar: \`${fstarVersionText}\``,
+              `- FStar commit: \`${fstarCommit}\``,
+              ``,
+              `### Run`,
+              `- Workflow run: ${process.env.RUN_URL}`
+            ].join('\n');
+
+            await github.graphql(
+              `mutation($repositoryId:ID!, $categoryId:ID!, $title:String!, $body:String!) {
+                createDiscussion(input:{
+                  repositoryId:$repositoryId,
+                  categoryId:$categoryId,
+                  title:$title,
+                  body:$body
+                }) {
+                  discussion { url }
+                }
+              }`,
+              {
+                repositoryId: categoryQuery.repository.id,
+                categoryId: category.id,
+                title: `FStar build with configurable Z3 inputs — ${date}`,
+                body
+              }
+            );