From ad4896c3e071e7e42f753aaffd742b471a1ac7b8 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Mon, 27 Jul 2026 12:14:58 -0700
Subject: [PATCH] Fix fstar-master-build.yml: use input defaults for scheduled
 runs (#10253)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

On scheduled runs, `github.event.inputs.*` is empty, so the `||
fallback` values in the `env` block are what actually get used — but two
of them diverged from the declared `workflow_dispatch` input defaults.

## Changes

- `Z3_RUNTIME_ARGS`: scheduled fallback was `smt.ho_matching=true`;
corrected to `smt.ho_matching=false` to match the input default
- `FSTAR_OTHERFLAGS`: scheduled fallback was `''`; corrected to
`--split_queries on_failure --log_failing_queries --ext higher_order_smt
--proof_recovery` to match the input default

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

diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml
index 69b33adbff..bfee2fc48c 100644
--- a/.github/workflows/fstar-master-build.yml
+++ b/.github/workflows/fstar-master-build.yml
@@ -49,10 +49,10 @@ jobs:
     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' }}
+      Z3_RUNTIME_ARGS: ${{ github.event.inputs.z3_runtime_args || 'smt.ho_matching=false' }}
       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 || '' }}
+      FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '--split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery' }}
       DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }}
     steps:
       - name: Checkout Z3