From 241c6211d6e0da7dd4ef8904314aa3db0775db30 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 6 Jun 2026 15:26:49 -0700
Subject: [PATCH] Fix build-and-report failure by removing unsupported default
 FStar HO-matching flag (#9748)

The `build-and-report` workflow failed in `build-and-report` because
FStar was invoked with a default `OTHERFLAGS` value containing
`--smt.ho_matching true`, which current FStar no longer recognizes. This
change removes that default while keeping the input configurable for
manual runs.

- **Root cause**
- Workflow default `fstar_otherflags` was set to `--smt.ho_matching
true`.
- During `make`, FStar exited with `error: unrecognized option
'--smt.ho_matching'` (job `79905082893`).

- **Workflow changes**
  - Updated `.github/workflows/fstar-master-build.yml`:
- `workflow_dispatch.inputs.fstar_otherflags.default` changed from
`--smt.ho_matching true` to `""`.
- Job env fallback `FSTAR_OTHERFLAGS` changed from `--smt.ho_matching
true` to `""`.
- Removed the outdated option example from the `fstar_otherflags` input
description.

- **Resulting behavior**
- Default scheduled/manual workflow runs no longer pass unsupported
FStar flags.
- Custom flags can still be provided via `fstar_otherflags` when needed.

```yaml
fstar_otherflags:
  description: "Extra FStar OTHERFLAGS"
  required: false
  default: ""

# ...
FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '' }}
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 .github/workflows/fstar-master-build.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml
index a3fd90c0e..518c67ec4 100644
--- a/.github/workflows/fstar-master-build.yml
+++ b/.github/workflows/fstar-master-build.yml
@@ -26,9 +26,9 @@ on:
         required: false
         default: "4.14.2"
       fstar_otherflags:
-        description: "Extra FStar OTHERFLAGS (example: --smt.ho_matching true)"
+        description: "Extra FStar OTHERFLAGS"
         required: false
-        default: "--smt.ho_matching true"
+        default: ""
       discussion_category:
         description: Discussion category name
         required: false
@@ -52,7 +52,7 @@ jobs:
       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' }}
+      FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '' }}
       DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }}
     steps:
       - name: Checkout Z3