mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-29 10:13:48 +00:00
Code Activity

Fix fstar-master-build.yml: use input defaults for scheduled runs (#10253)

Browse source 
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>
This commit is contained in:
Copilot 2026-07-27 12:14:58 -07:00 • committed by GitHub
parent 40d370b55b
commit ad4896c3e0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
.github/workflows/fstar-master-build.yml vendored
View file

@ -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