diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml
index 4b674fc33..f5b9417f2 100644
--- a/.github/workflows/fstar-master-build.yml
+++ b/.github/workflows/fstar-master-build.yml
@@ -86,6 +86,8 @@ jobs:
           /tmp/gh-aw/agent/z3-bin/z3 --version
 
       - name: Build FStar
+        id: build_fstar
+        continue-on-error: true
         run: |
           set -euo pipefail
           rm -rf /tmp/gh-aw/agent/FStar
@@ -106,18 +108,26 @@ jobs:
           /tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt
 
       - name: Create discussion summary
+        if: always()
         uses: actions/github-script@v9
         env:
           RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
         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 readIfExists = (path) => fs.existsSync(path) ? fs.readFileSync(path, 'utf8').trim() : null;
+            const z3VersionText = readIfExists('/tmp/gh-aw/agent/z3-version.txt') ?? 'unknown';
+            const fstarVersionFile = readIfExists('/tmp/gh-aw/agent/fstar-version.txt') ?? '';
             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 fstarCommitLine = readIfExists('/tmp/gh-aw/agent/fstar-commit.txt') ?? '';
+            const fstarCommit = fstarCommitLine ? fstarCommitLine.replace(/^FStar commit:\s*/, '') : 'unknown';
+            const fstarBuildOutcome = process.env.FSTAR_BUILD_OUTCOME || 'unknown';
+            const fstarBuildSucceeded = fstarBuildOutcome === 'success';
+            const fstarStatus = fstarBuildSucceeded
+              ? '✅ FStar build completed'
+              : `⚠️ FStar build ${fstarBuildOutcome} (pipeline continued)`;
             const date = new Date().toISOString().slice(0, 10);
 
             const owner = context.repo.owner;
@@ -146,7 +156,7 @@ jobs:
             const body = [
               `### Build status`,
               `- ✅ Z3 build completed`,
-              `- ✅ FStar build completed`,
+              `- ${fstarStatus}`,
               ``,
               `### Inputs used`,
               `- z3_ref: \`${process.env.Z3_REF}\``,