Merge branch 'Z3Prover:master' into master

2026-06-19 15:16:29 +00:00 · 2026-06-08 10:41:00 -07:00 · 2026-06-08 10:41:00 -07:00 · 20e09e7aeb
commit 20e09e7aeb
parent d2a782fb68 42e6ec5644
31 changed files with 514 additions and 1199 deletions
--- a/.github/agents/agentic-workflows.md
+++ b/.github/agents/agentic-workflows.md
@ -0,0 +1,224 @@
+---
+name: Agentic Workflows
+description: GitHub Agentic Workflows (gh-aw) - Create, debug, and upgrade AI-powered workflows with intelligent prompt routing.
+disable-model-invocation: true
+---
+
+# GitHub Agentic Workflows Agent
+
+This agent helps you work with **GitHub Agentic Workflows (gh-aw)**, a CLI extension for creating AI-powered workflows in natural language using markdown files.
+
+## What This Agent Does
+
+This is a **dispatcher agent** that routes your request to the appropriate specialized prompt based on your task:
+
+- **Creating new workflows**: Routes to `create` prompt
+- **Updating existing workflows**: Routes to `update` prompt
+- **Debugging workflows**: Routes to `debug` prompt
+- **Upgrading workflows**: Routes to `upgrade-agentic-workflows` prompt
+- **Creating report-generating workflows**: Routes to `report` prompt — consult this whenever the workflow posts status updates, audits, analyses, or any structured output as issues, discussions, or comments
+- **Creating shared components**: Routes to `create-shared-agentic-workflow` prompt
+- **Fixing Dependabot PRs**: Routes to `dependabot` prompt — use this when Dependabot opens PRs that modify generated manifest files (`.github/workflows/package.json`, `.github/workflows/requirements.txt`, `.github/workflows/go.mod`). Never merge those PRs directly; instead update the source `.md` files and rerun `gh aw compile --dependabot` to bundle all fixes
+- **Analyzing test coverage**: Routes to `test-coverage` prompt — consult this whenever the workflow reads, analyzes, or reports on test coverage data from PRs or CI runs
+- **Rendering ASCII charts in markdown**: Routes to `asciicharts` guide — consult this whenever the workflow needs compact charts that render reliably in GitHub issues, comments, or discussions
+- **CLI commands and triggering workflows**: Routes to `cli-commands` guide — consult this whenever the user asks how to run, compile, debug, or manage workflows from the command line, or when they need the MCP tool equivalent of a `gh aw` command
+- **Reducing token consumption / cost optimization**: Routes to `token-optimization` guide — consult this whenever the user asks how to reduce token usage, lower costs, speed up workflows, or measure the impact of prompt changes with experiments
+- **Choosing workflow architectures and design patterns**: Routes to `patterns` guide — consult this whenever the user asks for strategy, architecture, operating models, or pattern selection for agentic workflows
+
+Workflows may optionally include:
+
+- **Project tracking / monitoring** (GitHub Projects updates, status reporting)
+- **Orchestration / coordination** (one workflow assigning agents or dispatching and coordinating other workflows)
+
+## Files This Applies To
+
+- Workflow files: `.github/workflows/*.md` and `.github/workflows/**/*.md`
+- Workflow lock files: `.github/workflows/*.lock.yml`
+- Shared components: `.github/workflows/shared/*.md`
+- Configuration: `.github/aw/github-agentic-workflows.md`
+
+## Problems This Solves
+
+- **Workflow Creation**: Design secure, validated agentic workflows with proper triggers, tools, and permissions
+- **Workflow Debugging**: Analyze logs, identify missing tools, investigate failures, and fix configuration issues
+- **Version Upgrades**: Migrate workflows to new gh-aw versions, apply codemods, fix breaking changes
+- **Component Design**: Create reusable shared workflow components that wrap MCP servers
+
+## How to Use
+
+When you interact with this agent, it will:
+
+1. **Understand your intent** - Determine what kind of task you're trying to accomplish
+2. **Route to the right prompt** - Load the specialized prompt file for your task
+3. **Execute the task** - Follow the detailed instructions in the loaded prompt
+
+## Available Prompts
+
+### Create New Workflow
+**Load when**: User wants to create a new workflow from scratch, add automation, or design a workflow that doesn't exist yet
+
+**Prompt file**: `.github/aw/create-agentic-workflow.md`
+
+**Use cases**:
+- "Create a workflow that triages issues"
+- "I need a workflow to label pull requests"
+- "Design a weekly research automation"
+
+### Update Existing Workflow
+**Load when**: User wants to modify, improve, or refactor an existing workflow
+
+**Prompt file**: `.github/aw/update-agentic-workflow.md`
+
+**Use cases**:
+- "Add web-fetch tool to the issue-classifier workflow"
+- "Update the PR reviewer to use discussions instead of issues"
+- "Improve the prompt for the weekly-research workflow"
+
+### Debug Workflow
+**Load when**: User needs to investigate, audit, debug, or understand a workflow, troubleshoot issues, analyze logs, or fix errors
+
+**Prompt file**: `.github/aw/debug-agentic-workflow.md`
+
+**Use cases**:
+- "Why is this workflow failing?"
+- "Analyze the logs for workflow X"
+- "Investigate missing tool calls in run #12345"
+
+### Upgrade Agentic Workflows
+**Load when**: User wants to upgrade workflows to a new gh-aw version or fix deprecations
+
+**Prompt file**: `.github/aw/upgrade-agentic-workflows.md`
+
+**Use cases**:
+- "Upgrade all workflows to the latest version"
+- "Fix deprecated fields in workflows"
+- "Apply breaking changes from the new release"
+
+### Create a Report-Generating Workflow
+**Load when**: The workflow being created or updated produces reports — recurring status updates, audit summaries, analyses, or any structured output posted as a GitHub issue, discussion, or comment
+
+**Prompt file**: `.github/aw/report.md`
+
+**Use cases**:
+- "Create a weekly CI health report"
+- "Post a daily security audit to Discussions"
+- "Add a status update comment to open PRs"
+
+### Create Shared Agentic Workflow
+**Load when**: User wants to create a reusable workflow component or wrap an MCP server
+
+**Prompt file**: `.github/aw/create-shared-agentic-workflow.md`
+
+**Use cases**:
+- "Create a shared component for Notion integration"
+- "Wrap the Slack MCP server as a reusable component"
+- "Design a shared workflow for database queries"
+
+### Fix Dependabot PRs
+**Load when**: User needs to close or fix open Dependabot PRs that update dependencies in generated manifest files (`.github/workflows/package.json`, `.github/workflows/requirements.txt`, `.github/workflows/go.mod`)
+
+**Prompt file**: `.github/aw/dependabot.md`
+
+**Use cases**:
+- "Fix the open Dependabot PRs for npm dependencies"
+- "Bundle and close the Dependabot PRs for workflow dependencies"
+- "Update @playwright/test to fix the Dependabot PR"
+
+### Analyze Test Coverage
+**Load when**: The workflow reads, analyzes, or reports test coverage — whether triggered by a PR, a schedule, or a slash command. Always consult this prompt before designing the coverage data strategy.
+
+**Prompt file**: `.github/aw/test-coverage.md`
+
+**Use cases**:
+- "Create a workflow that comments coverage on PRs"
+- "Analyze coverage trends over time"
+- "Add a coverage gate that blocks PRs below a threshold"
+
+### CLI Commands Reference
+**Load when**: The user asks how to run, compile, debug, or manage workflows from the command line; needs the MCP tool equivalent of a `gh aw` command; or is in a restricted environment (e.g., Copilot Cloud) without direct CLI access.
+
+**Reference file**: `.github/aw/cli-commands.md`
+
+**Use cases**:
+- "How do I trigger workflow X on the main branch?"
+- "What's the MCP equivalent of `gh aw logs`?"
+- "I'm in Copilot Cloud — how do I compile a workflow?"
+- "Show me all available gh aw commands"
+
+### Token Consumption Optimization
+**Load when**: The user asks how to reduce token usage, lower workflow costs, make a workflow faster or cheaper, or measure the impact of prompt or configuration changes.
+
+**Reference file**: `.github/aw/token-optimization.md`
+
+**Use cases**:
+- "How do I reduce the token cost of this workflow?"
+- "My workflow is too expensive — how do I optimize it?"
+- "How do I compare token usage between two runs?"
+- "Should I use gh-proxy or the MCP server?"
+- "How do I use sub-agents to reduce costs?"
+- "How do I measure the impact of a prompt change?"
+
+### Workflow Pattern Selection
+**Load when**: The user asks for architecture, strategy, operating model selection, or pattern recommendations for building agentic workflows.
+
+**Reference file**: `.github/aw/patterns.md`
+
+**Use cases**:
+- "Which pattern should I use for multi-repo rollout?"
+- "How should I structure this workflow architecture?"
+- "What pattern fits slash-command triage?"
+- "Should this be DispatchOps or DailyOps?"
+
+## Instructions
+
+When a user interacts with you:
+
+1. **Identify the task type** from the user's request
+2. **Load the appropriate prompt** from the repository paths listed above
+3. **Follow the loaded prompt's instructions** exactly
+4. **If uncertain**, ask clarifying questions to determine the right prompt
+
+## Quick Reference
+
+```bash
+# Initialize repository for agentic workflows
+gh aw init
+
+# Generate the lock file for a workflow
+gh aw compile [workflow-name]
+
+# Trigger a workflow on demand (preferred over gh workflow run)
+gh aw run <workflow-name>             # interactive input collection
+gh aw run <workflow-name> --ref main  # run on a specific branch
+
+# Debug workflow runs
+gh aw logs [workflow-name]
+gh aw audit <run-id>
+
+# Upgrade workflows
+gh aw fix --write
+gh aw compile --validate
+```
+
+## Key Features of gh-aw
+
+- **Natural Language Workflows**: Write workflows in markdown with YAML frontmatter
+- **AI Engine Support**: Copilot, Claude, Codex, or custom engines
+- **MCP Server Integration**: Connect to Model Context Protocol servers for tools
+- **Safe Outputs**: Structured communication between AI and GitHub API
+- **Strict Mode**: Security-first validation and sandboxing
+- **Shared Components**: Reusable workflow building blocks
+- **Repo Memory**: Persistent git-backed storage for agents
+- **Sandboxed Execution**: All workflows run in the Agent Workflow Firewall (AWF) sandbox, enabling full `bash` and `edit` tools by default
+
+## Important Notes
+
+- Always reference the instructions file at `.github/aw/github-agentic-workflows.md` for complete documentation
+- Use the MCP tool `agentic-workflows` when running in GitHub Copilot Cloud
+- Workflows must be compiled to `.lock.yml` files before running in GitHub Actions
+- **Bash tools are enabled by default** - Don't restrict bash commands unnecessarily since workflows are sandboxed by the AWF
+- Follow security best practices: minimal permissions, explicit network access, no template injection
+- **Network configuration**: Use ecosystem identifiers (`node`, `python`, `go`, etc.) or explicit FQDNs in `network.allowed`. Bare shorthands like `npm` or `pypi` are **not** valid. See `.github/aw/network.md` for the full list of valid ecosystem identifiers and domain patterns.
+- **Single-file output**: When creating a workflow, produce exactly **one** workflow `.md` file. Do not create separate documentation files (architecture docs, runbooks, usage guides, etc.). If documentation is needed, add a brief `## Usage` section inside the workflow file itself.
+- **Triggering runs**: Always use `gh aw run <workflow-name>` to trigger a workflow on demand — not `gh workflow run <file>.lock.yml`. `gh aw run` handles workflow resolution by short name, input parsing and validation, and correct run-tracking for agentic workflows. Use `--ref <branch>` to run on a specific branch.
+- **CLI commands reference**: For a complete guide on all `gh aw` commands and their MCP tool equivalents (for restricted environments), see `.github/aw/cli-commands.md`
--- a/.github/mcp.json
+++ b/.github/mcp.json
@ -0,0 +1,11 @@
+{
+  "mcpServers": {
+    "github-agentic-workflows": {
+      "command": "gh",
+      "args": [
+        "aw",
+        "mcp-server"
+      ]
+    }
+  }
+}
--- a/.github/skills/agentic-workflows/SKILL.md
+++ b/.github/skills/agentic-workflows/SKILL.md
@ -0,0 +1,35 @@
+---
+name: agentic-workflows
+description: Route gh-aw workflow create/debug/upgrade requests to the right prompts.
+---
+
+# Agentic Workflows Router
+
+Use this skill when a user asks to create, update, debug, or upgrade GitHub Agentic Workflows in this repository.
+
+This skill is a dispatcher: identify the task type, load the matching `.github/aw/*.md` file, and follow it directly. Keep responses concise and ask a clarifying question if the correct prompt is unclear.
+
+Read only the files you need:
+Load these files from `github/gh-aw` (they are not available locally).
+- `.github/aw/create-agentic-workflow.md`
+- `.github/aw/create-shared-agentic-workflow.md`
+- `.github/aw/debug-agentic-workflow.md`
+- `.github/aw/github-agentic-workflows.md`
+- `.github/aw/update-agentic-workflow.md`
+- `.github/aw/upgrade-agentic-workflows.md`
+
+After loading the matching workflow prompt, follow it directly:
+- Create new workflows: `.github/aw/create-agentic-workflow.md`
+- Update existing workflows: `.github/aw/update-agentic-workflow.md`
+- Debug, audit, or investigate workflows: `.github/aw/debug-agentic-workflow.md`
+- Upgrade workflows and fix deprecations: `.github/aw/upgrade-agentic-workflows.md`
+- Create shared components or MCP wrappers: `.github/aw/create-shared-agentic-workflow.md`
+- Create report-generating workflows: `.github/aw/report.md`
+- Fix Dependabot manifest PRs: `.github/aw/dependabot.md`
+- Analyze coverage workflows: `.github/aw/test-coverage.md`
+- Render compact markdown charts: `.github/aw/asciicharts.md`
+- Map CLI commands to MCP usage: `.github/aw/cli-commands.md`
+- Choose workflow architecture and patterns: `.github/aw/patterns.md`
+- Optimize token usage and cost: `.github/aw/token-optimization.md`
+
+When the task involves OTEL, OTLP, traces, observability backends, or telemetry-driven analysis, also read and follow `skills/otel-queries/SKILL.md` after loading the matching workflow prompt.
--- a/.github/workflows/fstar-master-build.lock.yml
+++ b/.github/workflows/fstar-master-build.lock.yml
--- a/.github/workflows/fstar-master-build.md
+++ b/.github/workflows/fstar-master-build.md
@ -1,117 +0,0 @@
---
-description: Build Z3 master and then build FStar master using that Z3 build
-on:
-  schedule: daily
-  workflow_dispatch:
-permissions: read-all
-network: defaults
-tools:
-  bash: true
-timeout-minutes: 180
-steps:
-  - name: Checkout Z3 master
-    uses: actions/checkout@v6.0.2
-    with:
-      ref: master
-      fetch-depth: 1
-      persist-credentials: false
---
-
-# Build FStar master with Z3 master
-
-You are an AI build agent. Build the latest `master` branch of Z3, then build the latest `master` branch of FStar using the Z3 you just built.
-
-## Constraints
-
- Use `${{ github.workspace }}` as the workspace root.
- Put temporary files under `/tmp/gh-aw/agent`.
- Use only the Z3 built in this workflow when building FStar.
- Fail fast with clear error messages if any phase fails.
-
-## Phase 1: Build Z3 master
-
-```bash
-set -euo pipefail
-
-cd "${{ github.workspace }}"
-
-echo "Building Z3 from branch: $(git rev-parse --abbrev-ref HEAD)"
-git rev-parse HEAD
-
-sudo apt-get update -y
-sudo apt-get install -y cmake ninja-build python3 git curl unzip
-
-cmake -S . -B build/release -G Ninja -DCMAKE_BUILD_TYPE=Release
-ninja -C build/release z3
-
-"${{ github.workspace }}/build/release/z3" --version | tee /tmp/gh-aw/agent/z3-version.txt
-```
-
-Extract the numeric version string from the `z3 --version` output and store it in `Z3_VERSION` (for example, `4.15.4`).
-
-## Phase 2: Prepare PATH aliases for FStar
-
-FStar expects versioned Z3 command names on PATH. Create local aliases pointing to the Z3 binary from Phase 1.
-
-```bash
-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
-export PATH="/tmp/gh-aw/agent/z3-bin:$PATH"
-
-z3 --version
-z3-4.8.5 --version
-z3-4.13.3 --version
-```
-
-## Phase 3: Clone and build FStar master
-
-```bash
-set -euo pipefail
-
-mkdir -p /tmp/gh-aw/agent
-rm -rf /tmp/gh-aw/agent/FStar
-
-git clone --depth=1 --branch master https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar
-cd /tmp/gh-aw/agent/FStar
-
-echo "FStar commit: $(git rev-parse HEAD)"
-
-sudo apt-get update -y
-sudo apt-get install -y opam m4 pkg-config libgmp-dev
-
-opam init --disable-sandboxing --yes
-OPAM_SWITCH=4.14.2
-opam switch create "$OPAM_SWITCH" --yes || opam switch "$OPAM_SWITCH"
-eval "$(opam env --switch=$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)"
-if [ -z "$Z3_VERSION" ]; then
-  echo "ERROR: could not parse Z3 version from /tmp/gh-aw/agent/z3-version.txt"
-  exit 1
-fi
-
-echo "Using Z3 version override: $Z3_VERSION"
-PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="--z3version $Z3_VERSION" make -j"$(nproc)"
-```
-
-## Phase 4: Verify artifacts and report
-
-```bash
-set -euo pipefail
-
-test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe
-/tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt
-
-echo "SUCCESS: built Z3 master and FStar master with that Z3"
-```
-
-## Usage
-
- This workflow is scheduled daily and can also be started manually.
- It checks out Z3 `master`, builds `build/release/z3`, then clones FStar `master` and builds it using that Z3.
--- a/.github/workflows/fstar-master-build.yml
+++ 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: _nik_higher_order_smt
+      fstar_opam_switch:
+        description: OCaml switch for FStar build
+        required: false
+        default: "4.14.2"
+      fstar_otherflags:
+        description: "Extra FStar OTHERFLAGS"
+        required: false
+        default: "--split_queries --log_failing_queries --ext higher_order_smt --proof_recovery"
+      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 || '' }}
+      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 --recurse-submodules --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)" -k
+          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
+              }
+            );
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@ -7396,8 +7396,8 @@ class Statistics:
        >>> s.check()
        sat
        >>> st = s.statistics()
-        >>> len(st)
-        7
+        >>> len(st) > 0
+        True
        """
        return int(Z3_stats_size(self.ctx.ref(), self.stats))

@ -7410,8 +7410,8 @@ class Statistics:
        >>> s.check()
        sat
        >>> st = s.statistics()
-        >>> len(st)
-        7
+        >>> len(st) > 0
+        True
        >>> st[0]
        ('nlsat propagations', 2)
        >>> st[1]
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@ -507,6 +507,7 @@ class smt_printer {
        case forall_k: m_out << "forall "; break;
        case exists_k: m_out << "exists "; break;
        case lambda_k: m_out << "lambda "; break;
+        case choice_k: m_out << "choice "; break;
        }
        m_out << "(";
        for (unsigned i = 0; i < q->get_num_decls(); ++i) {
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@ -172,9 +172,7 @@ namespace sls {
                    return false;
                if (r > sx.length() && update(x, sx + zstring(random_char())))
                    return false;
-                // This case seems to imply unsat
-                verbose_stream() << "The input might be unsat\n"; // example to trigger: (assert (and (>= (str.len X) 2) (= (str.substr X 0 1) "")))
-                VERIFY(false);
+                // Both updates failed. Treat as unsatisfied and let outer search continue.
                return false;
            }

@ -198,8 +196,16 @@ namespace sls {
                return false;
            }
            if (seq.str.is_last_index(e, x, y) && seq.is_string(x->get_sort())) {
-                // TODO
-                NOT_IMPLEMENTED_YET();
+                auto sx = strval0(x);
+                auto sy = strval0(y);
+                rational val_e;
+                if (!a.is_numeral(ctx.get_value(e), val_e))
+                    return false;
+                rational actual(sx.last_indexof(sy));
+                if (val_e == actual)
+                    continue;
+                update(e, actual);
+                return false;
            }
            if (seq.str.is_stoi(e, x) && seq.is_string(x->get_sort())) {
                auto sx = strval0(x);
@ -753,7 +759,7 @@ namespace sls {
            for (unsigned j = 1; j <= val_other.length() - i; ++j) {
                zstring sub = val_other.extract(i, j);
                if (set.contains(sub))
-                    break;
+                    continue;
                set.insert(sub);
            }
        }
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@ -232,7 +232,9 @@ public:
                }
                ctx.validate_check_sat_result(r);
            }
-            t.collect_statistics(result->m_stats);
+            statistics stats;
+            t.collect_statistics(stats);
+            result->add_statistics(stats);
        }

        if (ctx.produce_unsat_cores()) {
--- a/src/muz/spacer/spacer_iuc_solver.cpp
+++ b/src/muz/spacer/spacer_iuc_solver.cpp
@ -185,7 +185,7 @@ namespace spacer {
        return m_base_defs.is_proxy (a, def);
    }

-    void iuc_solver::collect_statistics (statistics &st) const {
+    void iuc_solver::collect_statistics_core (statistics &st) const {
        m_solver.collect_statistics (st);
        st.update ("time.iuc_solver.get_iuc", m_iuc_sw.get_seconds());
        st.update ("time.iuc_solver.get_iuc.hyp_reduce1", m_hyp_reduce1_sw.get_seconds());
--- a/src/muz/spacer/spacer_iuc_solver.h
+++ b/src/muz/spacer/spacer_iuc_solver.h
@ -147,7 +147,7 @@ public:

    /* check_sat_result interface */

-    void collect_statistics(statistics &st) const override ;
+    void collect_statistics_core(statistics &st) const override ;
    virtual void reset_statistics();

    void get_unsat_core(expr_ref_vector &r) override;
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@ -1745,7 +1745,7 @@ namespace opt {
        m_pareto1 = p != nullptr;
    }

-    void context::collect_statistics(statistics& stats) const {
+    void context::collect_statistics_core(statistics& stats) const {
        if (m_solver) 
            m_solver->collect_statistics(stats);
        if (m_simplify) 
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@ -235,7 +235,7 @@ namespace opt {
        void get_model_core(model_ref& _m) override;
        void get_box_model(model_ref& _m, unsigned index) override;
        void fix_model(model_ref& _m) override;
-        void collect_statistics(statistics& stats) const override;
+        void collect_statistics_core(statistics& stats) const override;
        proof* get_proof_core() override { return nullptr; }
        void get_labels(svector<symbol> & r) override;
        void get_unsat_core(expr_ref_vector & r) override;
--- a/src/opt/opt_sls_solver.h
+++ b/src/opt/opt_sls_solver.h
@ -66,7 +66,7 @@ namespace opt {
        virtual void collect_param_descrs(param_descrs & r) {
            m_solver->collect_param_descrs(r);
        }
-        virtual void collect_statistics(statistics & st) const {
+        virtual void collect_statistics_core(statistics & st) const {
            m_solver->collect_statistics(st);
            if (m_bvsls) m_bvsls->collect_statistics(st);
            if (m_pbsls) m_pbsls->collect_statistics(st);
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@ -76,7 +76,7 @@ namespace opt {
        m_context.collect_param_descrs(r);
    }
    
-    void opt_solver::collect_statistics(statistics & st) const {        
+    void opt_solver::collect_statistics_core(statistics & st) const {        
        m_context.collect_statistics(st);
    }
    
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@ -89,7 +89,7 @@ namespace opt {
        solver* translate(ast_manager& m, params_ref const& p) override;
        void updt_params(params_ref const& p) override;
        void collect_param_descrs(param_descrs & r) override;
-        void collect_statistics(statistics & st) const override;
+        void collect_statistics_core(statistics & st) const override;
        void assert_expr_core(expr * t) override;
        void push_core() override;
        void pop_core(unsigned n) override;
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@ -387,7 +387,7 @@ public:
        if (p1.euf() && !get_euf()) 
            ensure_euf();        
    }
-    void collect_statistics(statistics & st) const override {
+    void collect_statistics_core(statistics & st) const override {
        if (m_preprocess) m_preprocess->collect_statistics(st);
        m_solver.collect_statistics(st);
    }
--- a/src/sat/sat_solver/sat_smt_solver.cpp
+++ b/src/sat/sat_solver/sat_smt_solver.cpp
@ -334,7 +334,7 @@ public:
            ensure_euf();
    }
    
-    void collect_statistics(statistics & st) const override {
+    void collect_statistics_core(statistics & st) const override {
        m_solver.collect_statistics(st);
    }
    
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@ -142,7 +142,7 @@ namespace {
            insert_ctrl_c(r);
        }

-        void collect_statistics(statistics & st) const override {
+        void collect_statistics_core(statistics & st) const override {
            m_context.collect_statistics(st);
        }

--- a/src/solver/check_sat_result.cpp
+++ b/src/solver/check_sat_result.cpp
@ -70,9 +70,6 @@ simple_check_sat_result::simple_check_sat_result(ast_manager & m):
    m_proof(m) {
    }

-void simple_check_sat_result::collect_statistics(statistics & st) const { 
-    st.copy(m_stats); 
-}

 void simple_check_sat_result::get_unsat_core(expr_ref_vector & r) { 
    if (m_status == l_false) {
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@ -46,6 +46,8 @@ protected:
    lbool       m_status = l_undef; 
    model_converter_ref m_mc0;
    double      m_time = 0;
+    statistics m_stats;
+
 public:
    check_sat_result(ast_manager& m): m(m), m_log(m), m_proof(m) {}
    virtual ~check_sat_result() = default;
@ -53,7 +55,18 @@ public:
    void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
    lbool set_status(lbool r) { return m_status = r; }
    lbool status() const { return m_status; }
-    virtual void collect_statistics(statistics & st) const = 0;
+    void collect_statistics(statistics &st) const {
+        collect_statistics_core(st);
+        st.copy(m_stats);       
+    }
+    void add_statistics(statistics const &st) {
+        m_stats.copy(st);
+    }
+    void reset_statistics() {
+        m_stats.reset();
+    }
+   
+    virtual void collect_statistics_core(statistics &st) const = 0;
    virtual void get_unsat_core(expr_ref_vector & r) = 0;
    void set_model_converter(model_converter* mc) { m_mc0 = mc; }
    model_converter* mc0() const { return m_mc0.get(); }
@ -92,7 +105,6 @@ public:
   \brief Very simple implementation of the check_sat_result object.
 */
 struct simple_check_sat_result : public check_sat_result {
-    statistics      m_stats;
    model_ref       m_model;
    expr_ref_vector m_core;
    proof_ref       m_proof;
@ -100,9 +112,9 @@ struct simple_check_sat_result : public check_sat_result {
    
    simple_check_sat_result(ast_manager & m);
    ast_manager& get_manager() const override { return m_proof.get_manager(); }
-    void collect_statistics(statistics & st) const override;
    void get_unsat_core(expr_ref_vector & r) override;
    void get_model_core(model_ref & m) override;
+    void collect_statistics_core(statistics &st) const override {}
    proof * get_proof_core() override;
    std::string reason_unknown() const override;
    void get_labels(svector<symbol> & r) override;
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@ -290,7 +290,7 @@ public:
        return m_solver1->display(out, n, es);
    }

-    void collect_statistics(statistics & st) const override {
+    void collect_statistics_core(statistics & st) const override {
        m_solver2->collect_statistics(st);
        if (m_use_solver1_results)
            m_solver1->collect_statistics(st);
--- a/src/solver/simplifier_solver.cpp
+++ b/src/solver/simplifier_solver.cpp
@ -229,7 +229,7 @@ public:
        return s->check_sat_core(num_assumptions, _assumptions.data()); 
    }

-    void collect_statistics(statistics& st) const override { 
+    void collect_statistics_core(statistics& st) const override { 
        s->collect_statistics(st); 
        m_preprocess.collect_statistics(st);
    }
--- a/src/solver/slice_solver.cpp
+++ b/src/solver/slice_solver.cpp
@ -319,7 +319,7 @@ public:
        return s->check_sat_core(num_assumptions, assumptions);
    }

-    void collect_statistics(statistics& st) const override { s->collect_statistics(st); }
+    void collect_statistics_core(statistics& st) const override { s->collect_statistics(st); }

    void get_model_core(model_ref& mdl) override { s->get_model_core(mdl); }

--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@ -83,7 +83,7 @@ public:
    void pop_params() override {m_base->pop_params();}
    
    void collect_param_descrs(param_descrs & r) override { m_base->collect_param_descrs(r); }
-    void collect_statistics(statistics & st) const override { m_base->collect_statistics(st); }
+    void collect_statistics_core(statistics & st) const override { m_base->collect_statistics(st); }
    unsigned get_num_assertions() const override { return m_base->get_num_assertions(); }
    expr * get_assertion(unsigned idx) const override { return m_base->get_assertion(idx); }

--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@ -49,7 +49,7 @@ class tactic2solver : public solver_na2as {
    bool                         m_produce_models;
    bool                         m_produce_proofs;
    bool                         m_produce_unsat_cores;
-    statistics                   m_stats;
+//    statistics                   m_stats;
    bool                         m_minimizing = false;
    
 public:
@ -70,7 +70,7 @@ public:
    void pop_core(unsigned n) override;
    lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override;

-    void collect_statistics(statistics & st) const override;
+    void collect_statistics_core(statistics & st) const override;
    void get_unsat_core(expr_ref_vector & r) override;
    void get_model_core(model_ref & m) override;
    proof * get_proof_core() override;
@ -284,8 +284,9 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
        m_result->m_unknown = ex.what();
        m_result->m_proof = pr;
    }
-    m_tactic->collect_statistics(m_result->m_stats);
-    m_tactic->collect_statistics(m_stats);
+    statistics stats;
+    m_tactic->collect_statistics(stats);
+    m_result->add_statistics(stats);
    m_result->m_model = md;
    m_result->m_proof = pr;
    if (m_produce_unsat_cores) {
@ -311,7 +312,7 @@ solver* tactic2solver::translate(ast_manager& m, params_ref const& p) {
 }


-void tactic2solver::collect_statistics(statistics & st) const {    
+void tactic2solver::collect_statistics_core(statistics & st) const {    
    st.copy(m_stats);
    if (m_stats.size() == 0 && m_tactic)
        m_tactic->collect_statistics(st);
--- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp
+++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
@ -159,7 +159,7 @@ public:
    void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); }
    void set_produce_models(bool f) override { m_solver->set_produce_models(f); }
    void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback);  }
-    void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); }
+    void collect_statistics_core(statistics & st) const override { m_solver->collect_statistics(st); }
    void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
    void set_phase(expr* e) override { m_solver->set_phase(e); }
    phase* get_phase() override { return m_solver->get_phase(); }
--- a/src/tactic/fd_solver/enum2bv_solver.cpp
+++ b/src/tactic/fd_solver/enum2bv_solver.cpp
@ -85,7 +85,7 @@ public:
    void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); }    
    void set_produce_models(bool f) override { m_solver->set_produce_models(f); }
    void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback);  }
-    void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); }
+    void collect_statistics_core(statistics & st) const override { m_solver->collect_statistics(st); }
    void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
    void set_phase(expr* e) override { m_solver->set_phase(e); }
    phase* get_phase() override { return m_solver->get_phase(); }
--- a/src/tactic/fd_solver/pb2bv_solver.cpp
+++ b/src/tactic/fd_solver/pb2bv_solver.cpp
@ -82,7 +82,7 @@ public:
    void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); m_rewriter.collect_param_descrs(r);}    
    void set_produce_models(bool f) override { m_solver->set_produce_models(f); }
    void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback);  }
-    void collect_statistics(statistics & st) const override { 
+    void collect_statistics_core(statistics & st) const override { 
        m_rewriter.collect_statistics(st);
        m_solver->collect_statistics(st); 
    }
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@ -2032,7 +2032,7 @@ namespace smtfd {

        void set_produce_models(bool f) override { }
        void set_progress_callback(progress_callback * callback) override { }
-        void collect_statistics(statistics & st) const override {
+        void collect_statistics_core(statistics & st) const override {
            if (m_fd_sat_solver) {
                m_fd_sat_solver->collect_statistics(st); 
                m_fd_core_solver->collect_statistics(st);