{"owner":"Z3Prover","repo":"z3","hasSkills":true,"totalSkillsCount":13,"totalTokensCount":13478,"categories":["copilot-instructions","anthropic-skill"],"hasMcp":false,"mcpConfig":null,"found":[".github/copilot-instructions.md",".github/skills/README.md",".github/skills/agentic-workflow-designer/SKILL.md",".github/skills/agentic-workflows/SKILL.md",".github/skills/benchmark/SKILL.md",".github/skills/encode/SKILL.md",".github/skills/explain/SKILL.md",".github/skills/memory-safety/SKILL.md",".github/skills/optimize/SKILL.md",".github/skills/prove/SKILL.md",".github/skills/simplify/SKILL.md",".github/skills/solve/SKILL.md",".github/skills/static-analysis/SKILL.md"],"skills":{".github/copilot-instructions.md":"# Z3 Theorem Prover Development Guide\n\nAlways reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here.\n\n## Working Effectively\n\n### Bootstrap and Build the Repository\n\nZ3 is built with CMake:\n- `cmake -S . -B build` -- takes 1 second to configure\n- `cmake --build build --parallel $(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Dependencies and Requirements\n- Python 3.x (required to run CMake's code generation scripts)\n- C++20 capable compiler (g++ or clang++)\n- Git (for version information)\n\n### Test the Repository\n\n- Build unit tests: `cmake --build build --target test-z3 --parallel $(nproc)` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**Test basic Z3 functionality:**\n```bash\n./z3 --version\necho \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\" | ./z3 -in\n```\n\n### Validation Scenarios\n\n**ALWAYS** test these scenarios after making changes:\n\n#### Basic SMT Solving\n```bash\ncd build\necho \"(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(get-model)\" | ./z3 -in\n```\nExpected output: `sat` followed by a model showing `x = 1` or similar.\n\n#### Python Bindings\n```bash\ncd build/python\npython3 -c \"import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())\"\n```\nExpected output: `Result: sat` and `Model: [x = 1]` or similar.\n\n#### Command Line Help\n```bash\n./z3 --help | head -10\n```\nShould display version and usage information.\n\n## Build System Details\n\n### CMake Build System\n- Configuration: `cmake -S . -B build` (1 second)\n- Main build: `cmake --build build --parallel $(nproc)` (17 minutes)\n- Creates Python bindings in `build/python/` when `-DZ3_BUILD_PYTHON_BINDINGS=ON` is set\n- Out-of-source build: clean build tree, no source pollution\n\n### Critical Timing and Timeout Requirements\n\n**NEVER CANCEL these operations**:\n- `cmake --build build --parallel $(nproc)`: 15-17 minutes. **Set timeout to 30+ minutes minimum**.\n- `cmake --build build --target test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**.\n- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**.\n\n**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing.\n\n## Repository Structure\n\n### Key Directories\n- `src/` - Main source code organized by components (ast, smt, sat, etc.)\n- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.)\n- `scripts/` - Build scripts and utilities\n- `.github/workflows/` - CI/CD pipeline definitions\n- `cmake/` - CMake configuration files\n\n### Important Files\n- `README.md` - Main documentation and build instructions\n- `README-CMake.md` - Detailed CMake build documentation\n- `CMakeLists.txt` - Main CMake configuration\n\n## Common Tasks and Validation\n\n### Pre-commit Validation\nBefore committing changes:\n1. **Build successfully**: Use one of the validated build commands above\n2. **Run unit tests**: `./test-z3 /a` must pass\n3. **Test basic functionality**: Run validation scenarios above\n4. **Test affected language bindings**: If modifying API, test relevant examples\n\n### Working with Language Bindings\n- **Python**: Located in `build/python/`, test with validation scenario above\n- **C/C++**: Examples in `examples/c/` and `examples/c++/`\n  - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example`\n  - Run with: `LD_LIBRARY_PATH=build ./test_example`\n- **Java**: Build with `cmake -S . -B build -DZ3_BUILD_JAVA_BINDINGS=ON`, examples in `examples/java/`\n- **C#/.NET**: Build with `cmake -S . -B build -DZ3_BUILD_DOTNET_BINDINGS=ON`, examples in `examples/dotnet/`\n\n### Performance Testing\nFor performance-sensitive changes:\n- Build optimized: `cmake -S . -B build -DCMAKE_BUILD_TYPE=Release` (Release mode)\n- Test with realistic SMT problems from `examples/SMT-LIB2/`\n- Use Z3's built-in statistics: `z3 -st problem.smt2`\n\n## Common Issues and Solutions\n\n### Python Import Errors\n- **Error**: `import z3` fails\n- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH`\n\n### Missing Dependencies\n- **Error**: Compiler not found or version too old\n- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+\n\n### Long Build Times\n- **Normal**: 15-17 minute builds are expected for Z3\n- **Never cancel**: Set timeouts appropriately and wait for completion\n- **Optimization**: Use `cmake --build build --parallel $(nproc)` for parallel compilation\n\n## Key Projects in Codebase\n\nZ3 is organized into several key components:\n\n- **Core SMT**: `src/smt/` - Main SMT solver engine\n- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver  \n- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.)\n- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation\n- **Tactics**: `src/tactic/` - Configurable solving strategies\n- **API**: `src/api/` - Public C API and language bindings\n- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers\n- **Model Generation**: Creating and manipulating satisfying assignments\n\nThe architecture is modular with clean separation between the core solver, theory plugins, and user interfaces.\n",".github/skills/README.md":"# Z3 Agent Skills\n\nReusable, composable verification primitives for the Z3 theorem prover.\nEach skill is a self-contained unit: a `SKILL.md` prompt that guides the\nLLM agent, backed by a Python validation script in `scripts/`.\n\n## Skill Catalogue\n\n| Skill | Status | Description |\n|-------|--------|-------------|\n| solve | implemented | Check satisfiability of SMT-LIB2 formulas; return models or unsat cores |\n| prove | implemented | Prove validity by negation and satisfiability checking |\n| encode | implemented | Translate constraint problems into SMT-LIB2 or Z3 Python API code |\n| simplify | implemented | Reduce formula complexity using configurable Z3 tactic chains |\n| optimize | implemented | Solve constrained optimization (minimize/maximize) over numeric domains |\n| explain | implemented | Parse and interpret Z3 output: models, cores, statistics, errors |\n| benchmark | implemented | Measure Z3 performance and collect solver statistics |\n| static-analysis | implemented | Run Clang Static Analyzer on Z3 source and log structured findings |\n| memory-safety | implemented | Run ASan/UBSan on Z3 test suite to detect memory errors and undefined behavior |\n\n## Agent\n\nA single orchestration agent composes these skills into end-to-end workflows:\n\n| Agent | Role |\n|-------|------|\n| z3 | SMT solving, code quality analysis, and stress testing |\n\n## Shared Infrastructure\n\nAll scripts share a common library at `shared/z3db.py` with:\n\n* `Z3DB`: SQLite wrapper for tracking runs, formulas, findings, and interaction logs.\n* `run_z3()`: Pipe SMT-LIB2 into `z3 -in` with timeout handling.\n* `find_z3()`: Locate the Z3 binary across build directories and PATH.\n* Parsers: `parse_model()`, `parse_stats()`, `parse_unsat_core()`.\n\nThe database schema lives in `shared/schema.sql`.\n\n## Relationship to a3/ Workflows\n\nThe `a3/` directory at the repository root contains two existing agentic workflow\nprompts that predate the skill architecture:\n\n* `a3/a3-python.md`: A3 Python Code Analysis agent (uses the a3-python pip tool\n  to scan Python source, classifies findings, creates GitHub issues).\n* `a3/a3-rust.md`: A3 Rust Verifier Output Analyzer (downloads a3-rust build\n  artifacts, parses bug reports, creates GitHub discussions).\n\nThese workflows are complementary to the skills defined here, not replaced by\nthem. The a3 prompts focus on external analysis tooling and GitHub integration,\nwhile skills focus on Z3 solver operations and their validation. Both may be\ncomposed by the same orchestrating agent.\n\n## Usage\n\nCheck database status and recent runs:\n\n```\npython shared/z3db.py status\npython shared/z3db.py runs --skill solve --last 5\npython shared/z3db.py log --run-id 12\npython shared/z3db.py query \"SELECT skill, COUNT(*) FROM runs GROUP BY skill\"\n```\n\nRun an individual skill script directly:\n\n```\npython solve/scripts/solve.py --file problem.smt2\npython encode/scripts/encode.py --validate formula.smt2\npython benchmark/scripts/benchmark.py --file problem.smt2\n```\n",".github/skills/agentic-workflow-designer/SKILL.md":"---\nname: agentic-workflow-designer\ndescription: Conversational skill that interviews users to design new agentic workflows\ndisable-model-invocation: true\n---\n\n# Workflow Designer\n\nUse this skill to run a structured interview with users who know their goal but not the workflow syntax yet, then generate one complete workflow `.md` file.\n\n## When to Use This Skill\n\nUse this before `.github/aw/create-agentic-workflow.md` when requirements are unclear or incomplete.\n\n- Use `skills/agentic-workflow-designer/SKILL.md` to discover and confirm requirements.\n- Use `.github/aw/create-agentic-workflow.md` once requirements are clear and ready for implementation.\n- Use `.github/aw/agentic-chat.md` when the user wants a specification/pseudo-code instead of a runnable workflow file.\n\n## Interview Framework\n\nAsk one question at a time. Move to the next phase only after the current phase is clear.\n\n### Phase 1: Goal\n\nAsk: **\"What do you want to automate?\"**\n\nCapture:\n- Workflow name (kebab-case candidate)\n- Brief description\n- Optional emoji\n\n### Phase 2: Trigger\n\nAsk: **\"When should this run?\"**\n\nFollow up only if needed:\n- Which event type(s)?\n- Any filters (labels, branches, commands)?\n- Scheduled cadence (daily/weekly/hourly)?\n\nMap to the `on:` block.\n\n### Phase 3: Scope (Read/Write)\n\nAsk:\n- **\"What should it read?\"** (issues, PRs, code, discussions, CI data)\n- **\"What should it create or update?\"** (comments, issues, PRs, labels)\n\nMap to:\n- `permissions:` (keep read-only for agent job)\n- `tools:`\n- `safe-outputs:`\n\n### Phase 4: Data Strategy\n\nAsk:\n- **\"What data does the agent need to make decisions?\"**\n- Follow up: **\"Can we pre-fetch and aggregate that data with shell commands so the agent only reads compact JSON?\"**\n\nCapture:\n- Whether `steps:` should pre-fetch GitHub data with `gh` + `jq`\n- Output paths under `/tmp/gh-aw/data/`\n- Whether batch work should use sub-agents\n\nMap to:\n- `steps:`\n- Prompt references to pre-computed file paths\n\n### Phase 5: Guardrails\n\nAsk: **\"Should it block merging, just advise, or silently log?\"**\n\nCapture:\n- Visibility expectations (comment, issue, no visible output)\n- No-op behavior expectation\n\nGuide toward safe output behavior and explicit `noop` instructions.\n\n### Phase 6: Context & Network\n\nAsk: **\"Does it need external APIs, web access, package installs, or MCP servers?\"**\n\nFollow up:\n- **\"Any third-party services or MCP servers to include (for example Slack, Jira, Datadog, custom internal MCP)?\"**\n- **\"Are you deploying on GitHub.com, GHEC with custom endpoints, or GHES?\"**\n- For each integration, identify required auth from source docs and map it to GitHub Actions secrets + workflow env variables.\n- Ask for exact external domains (FQDN/wildcard).\n\nMap to:\n- `network.allowed`\n- Optional MCP/GitHub tool usage in `tools:`\n- `secrets:` / `env:` wiring for integration tokens\n- GHES/GHEC settings such as `engine.api-target` and `aw.json` `ghes: true` (when applicable)\n\n### Phase 7: Engine (optional)\n\nAsk only if ambiguous: **\"Any AI engine preference?\"**\n\nIf no preference, suggest default:\n- \"I'd suggest Copilot since you haven't mentioned a preference. Sound good?\"\n\nMap to `engine:` only when not default.\n\n### Phase 8: Confirmation\n\nPresent a structured summary and ask for approval before generation.\n\n## Decision Heuristics\n\n### Trigger Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"when someone opens a PR\" | `on: pull_request:` with `types: [opened]` |\n| \"when a PR is updated\" | `on: pull_request:` with `types: [opened, synchronize]` |\n| \"every morning\", \"daily\" | fuzzy schedule shorthand `on: schedule: daily on weekdays` (compiler expands to cron) |\n| \"every Monday\", \"weekly\" | fuzzy schedule shorthand `on: schedule: weekly` (compiler expands to cron) |\n| \"when I say /review\" | `on: slash_command:` with `name: review` (or requested command) |\n| \"when an issue is labeled bug\" | `on: issues:` with `types: [labeled]` and label filter guidance |\n| \"run when label ai-review is added\" | `on: label_command:` with `name`/`names`, optional event scoping, and label-as-command semantics |\n| \"run on PRs from forks\" | `on: pull_request:` plus explicit `forks:` allowlist and fork security guardrails |\n| \"sometimes automatic, sometimes manual\" | semi-active pattern: combine `schedule`/event triggers with `workflow_dispatch` |\n| \"manually\", \"on demand\" | `on: workflow_dispatch:` |\n| \"when a deployment fails\" | `on: deployment_status:` |\n| \"when another workflow finishes\" | `on: workflow_run:` |\n\n### Safe Output Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"post a comment\" | `add-comment` |\n| \"create an issue\" | `create-issue` |\n| \"update issue title/body\" | `update-issue` |\n| \"close the issue\" | `close-issue` |\n| \"assign someone\", \"remove assignment\" | `assign-to-user`, `unassign-from-user` |\n| \"set issue type/field/milestone\" | `set-issue-type`, `set-issue-field`, `assign-milestone` |\n| \"open a PR\", \"submit changes\" | `create-pull-request` |\n| \"update PR description/title\" | `update-pull-request` |\n| \"close the PR\", \"merge the PR\" | `close-pull-request`, `merge-pull-request` |\n| \"mark PR ready\", \"sync PR branch\" | `mark-pull-request-as-ready-for-review`, `update-branch` |\n| \"commit a fix to the PR branch\" | `push-to-pull-request-branch` |\n| \"approve / request changes\" | `submit-pull-request-review` |\n| \"inline review comment\", \"reply to review thread\" | `create-pull-request-review-comment`, `reply-to-pull-request-review-comment`, `resolve-pull-request-review-thread` |\n| \"start or edit discussion\", \"close discussion\" | `create-discussion`, `update-discussion`, `close-discussion` |\n| \"request reviewer\", \"hide comment\" | `add-reviewer`, `hide-comment` |\n| \"create/update project\", \"project status update\" | `create-project`, `update-project`, `create-project-status-update` |\n| \"update release\", \"upload release asset\" | `update-release`, `upload-asset` |\n| \"create/auto-fix code scan alert\" | `create-code-scanning-alert`, `autofix-code-scanning-alert` |\n| \"start an agent session\", \"assign to an agent\" | `create-agent-session`, `assign-to-agent` |\n| \"store persistent memory comment\" | `comment-memory` |\n| \"link a sub-issue\" | `link-sub-issue` |\n| \"add labels\", \"remove labels\" | `add-labels`, `remove-labels` |\n| \"nothing visible\", \"just analyze\" | no safe outputs required |\n\n### Network Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"calls an external API\" | ask for exact FQDN/wildcard, then add to `network.allowed` |\n| \"reads GitHub data / clones repos\" | include `github` in `network.allowed` |\n| \"uses GitHub Actions artifacts or cache\" | include `github-actions` in `network.allowed` |\n| \"installs npm packages\" | include `node` in `network.allowed` |\n| \"runs pip install\" | include `python` in `network.allowed` |\n| \"builds Go code\" | include `go` in `network.allowed` |\n| \"installs gems / uses Bundler\" | include `ruby` in `network.allowed` |\n| \"runs cargo build\" | include `rust` in `network.allowed` |\n| \"uses NuGet / .NET restore\" | include `dotnet` in `network.allowed` |\n| \"builds with Maven / Gradle\" | include `java` in `network.allowed` |\n| \"uses Docker / pulls container images / pushes to GHCR\" | include `containers` in `network.allowed` |\n| \"runs Playwright browser tests\" | include `playwright` in `network.allowed` |\n| \"runs apt install / yum / apk\" | include `linux-distros` in `network.allowed` |\n| \"uses Terraform / HashiCorp registry\" | include `terraform` in `network.allowed` |\n| \"connects to localhost / loopback / local services\" | include `local` in `network.allowed` |\n| \"uses Swift Package Manager\" | include `swift` in `network.allowed` |\n| \"uses Composer / PHP packages\" | include `php` in `network.allowed` |\n| \"uses pub.dev / Dart packages\" | include `dart` in `network.allowed` |\n| \"uses Hackage / Haskell packages\" | include `haskell` in `network.allowed` |\n| \"uses CPAN / Perl packages\" | include `perl` in `network.allowed` |\n| \"serves or loads web fonts\" | include `fonts` in `network.allowed` |\n| \"uses Deno or JSR packages\" | include `deno` in `network.allowed` |\n| \"uses Elixir / Hex packages\" | include `elixir` in `network.allowed` |\n| \"uses Bazel build\" | include `bazel` in `network.allowed` |\n| \"uses R / CRAN packages\" | include `r` in `network.allowed` |\n| \"no external access\" | `network.allowed: [defaults]` (or `[]` if explicitly zero network) |\n\n### Tool Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"read GitHub issues/PRs/workflows\" | `tools.github` with `mode: gh-proxy` and minimal `toolsets` |\n| \"use full MCP server/tool definitions\" | `tools.github` with `mode: local` |\n| \"use other MCP servers but keep token cost down\" | `tools.cli-proxy: true` (hybrid CLI-proxy mode) |\n| \"edit files\" | `edit` tool (default unless restricted) |\n| \"run commands/tests\" | `bash` tool (default unless restricted) |\n| \"browse web pages/docs\" | `web-fetch` and/or `web-search` |\n| \"test UI flows\" | `playwright` |\n\n### Pattern Heuristics\n\n| User says... | Recommended named pattern |\n|---|---|\n| \"triage issues automatically\" | `IssueOps` |\n| \"run on /commands with human approval loops\" | `ChatOps` |\n| \"run every weekday and keep improving\" | `DailyOps` |\n| \"monitor workflow failures and trends\" | `MonitorOps` |\n| \"process a big backlog in chunks\" | `BatchOps` |\n| \"run manually with input parameters\" | `DispatchOps` |\n| \"apply a label-based workflow\" | `LabelOps` |\n| \"operate across multiple repositories\" | `MultiRepoOps` |\n| \"coordinate multiple sub-agents\" | `Orchestration` |\n| \"manage project board items\" | `ProjectOps` |\n| \"research, plan, and assign issues\" | `ResearchPlanAssignOps` |\n| \"self-correcting / retry on failure\" | `CorrectionOps` |\n| \"run in a side/fork repo\" | `SideRepoOps` |\n| \"write a spec before implementing\" | `SpecOps` |\n| \"A/B test workflow variants\" | `TrialOps` |\n| \"process items from a queue\" | `WorkQueueOps` |\n| \"deterministic, no LLM needed\" | `DeterministicOps` |\n| \"manage from a central repo\" | `CentralRepoOps` |\n| \"track work via GitHub Projects\" | `Monitoring with Projects` |\n\n### Integration Auth Mapping\n\nWhen the user names a third-party service or MCP server:\n\n1. Confirm whether native tool, MCP server, or safe-output job is the right integration path.\n2. Look up the integration's auth requirements and required scopes before finalizing the design.\n3. Provide a concrete setup checklist with:\n   - required GitHub Actions secrets (names to create)\n   - workflow env variables that consume those secrets\n   - minimum token scopes/permissions needed\n\nOutput format to use:\n\n```text\nIntegration auth setup:\n- <service-or-mcp>: <purpose>\n  - Secrets to create: <SECRET_NAME>, <SECRET_NAME>\n  - Workflow env vars: <ENV_VAR>=${{ secrets.<SECRET_NAME> }}\n  - Required scopes/permissions: <least-privilege scopes>\n```\n\nNever suggest committing plaintext tokens.\n\n### Data Strategy Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"analyze PRs\", \"review issues\", \"check status\" | add `steps:` that pre-fetch with `gh` + `jq` |\n| \"read the diff\", \"look at changed files\" | add `steps:` using `gh pr diff` or `gh pr view --json files` |\n| \"search for patterns across repos\" | add `steps:` using `gh search` + `jq` filters |\n| \"just respond to a comment\" | no pre-fetch needed (event payload is enough) |\n| \"process each item individually\" | suggest sub-agent pattern with `model: small` |\n\n## Token Optimization Defaults\n\nApply these defaults unless the user explicitly asks otherwise:\n\n1. Use DataOps by default for GitHub reads: pre-fetch/aggregate with `gh` + `jq` in `steps:`, store compact JSON in `/tmp/gh-aw/data/`, and point the prompt to those files (see `.github/aw/token-optimization.md` for details).\n2. Keep tool surface minimal: default to `tools.github.mode: gh-proxy`, include only required toolsets, and prefer `bash` + `gh` for simple reads.\n3. For batch workloads, split items into compact data and suggest sub-agent processing with `model: small`.\n4. Keep prompts compact: concise imperative instructions, explicit file paths, single-line `noop` guidance, and stable instructions before dynamic content.\n\n## Progressive Disclosure Rules\n\n1. Never dump all options at once; ask one targeted question at a time.\n2. Skip questions when answers are inferable from prior user statements.\n3. Offer smart defaults and request confirmation instead of over-questioning.\n4. Ask at most 5 questions before presenting a summary; then ask \"anything else?\" if needed.\n5. Detect done signals (`that's it`, `looks good`, `generate it`) and proceed to generation.\n\n## Confirmation Format\n\nUse this exact structure:\n\n```text\n📋 Proposed workflow:\n- Name: <workflow-id>\n- Trigger: <event + key options>\n- Engine: <engine or default>\n- Tools: <tool summary>\n- Safe outputs: <list or none>\n- Network: <allowed summary>\n- Integrations/Auth: <service/mcp + required secrets/env vars>\n- Deployment: <GitHub.com or GHEC/GHES details>\n- Intent: <one-sentence task>\n```\n\nThen ask: **\"Ready to generate, or want to adjust anything?\"**\n\n## Generation Template\n\nAfter confirmation, generate one workflow file using the same skeleton style as `.github/aw/create-agentic-workflow.md`.\n\n```markdown\n---\nemoji: <emoji>\ndescription: <brief description>\non:\n  <trigger config>\npermissions:\n  contents: read\n  issues: read\n  pull-requests: read\ntools:\n  github:\n    mode: gh-proxy\n    toolsets: [default]\nsteps:\n  - name: <optional data prefetch>\n    run: |\n      mkdir -p /tmp/gh-aw/data\n      <gh + jq commands that produce compact JSON>\nsafe-outputs:\n  <safe-output-types-if-needed>\nnetwork:\n  allowed:\n    - defaults\n    - <additional entries if needed>\n---\n\n# <Workflow Name>\n\n## Task\n\n<clear instructions tied to trigger context>\nIf `steps:` includes pre-fetch commands, read the resulting `/tmp/gh-aw/data/*.json` files instead of broad live re-fetches.\n\n## Safe Outputs\n\n- Use configured safe outputs for all visible write actions.\n- Call `noop` with a short reason when no action is needed.\n```\n\n## Validation Checklist\n\nBefore final output, run this internal self-check:\n\n- [ ] Agent job permissions remain read-only (writes only via safe outputs)\n- [ ] `safe-outputs:` covers every write action mentioned in prompt/instructions\n- [ ] Network access is scoped; avoid blanket wildcard entries\n- [ ] Trigger matches the user's intended activation event\n- [ ] Prompt instructs agent to call `noop` when no action is needed\n- [ ] Unnecessary defaults are omitted (for example `engine: copilot`)\n- [ ] If reading GitHub data, `steps:` pre-fetches compact JSON (DataOps)\n- [ ] `tools.github.mode` is `gh-proxy` unless broader MCP toolsets are explicitly needed\n- [ ] Only required toolsets are listed (avoid blanket toolset lists)\n- [ ] Prompt references specific pre-computed file paths\n- [ ] For batch processing (>5 items), sub-agent pattern is suggested\n- [ ] For each third-party service/MCP integration, required secrets/env vars are listed\n- [ ] Auth guidance includes least-privilege token scope recommendations\n- [ ] For GHEC/GHES deployments, `engine.api-target` and GHES compatibility guidance are included when needed\n\n## References (load only when needed)\n\nIn-repo references:\n- `.github/aw/syntax.md` (index → `.github/aw/syntax-core.md`, `.github/aw/syntax-agentic.md`, `.github/aw/syntax-tools-imports.md`)\n- `.github/aw/safe-outputs.md` (index → `.github/aw/safe-outputs-content.md`, `.github/aw/safe-outputs-management.md`, `.github/aw/safe-outputs-automation.md`, `.github/aw/safe-outputs-runtime.md`)\n- `.github/aw/network.md`\n- `.github/aw/patterns.md`\n- `.github/aw/subagents.md`\n- `.github/aw/token-optimization.md`\n- `.github/aw/triggers.md`\n- `.github/aw/create-agentic-workflow.md`\n\nPortable HTTPS references:\n- `https://github.com/github/gh-aw/blob/main/.github/aw/syntax.md` (index → `.../syntax-core.md`, `.../syntax-agentic.md`, `.../syntax-tools-imports.md`)\n- `https://github.com/github/gh-aw/blob/main/.github/aw/safe-outputs.md` (index → `.../safe-outputs-content.md`, `.../safe-outputs-management.md`, `.../safe-outputs-automation.md`, `.../safe-outputs-runtime.md`)\n- `https://github.com/github/gh-aw/blob/main/.github/aw/network.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/patterns.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/triggers.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/create-agentic-workflow.md`\n",".github/skills/agentic-workflows/SKILL.md":"---\nname: agentic-workflows\ndescription: Route gh-aw workflow design/create/debug/upgrade requests to the right prompts.\n---\n\n# Agentic Workflows Router\n\nUse this skill when a user asks to design, create, update, debug, or upgrade GitHub Agentic Workflows in this repository.\n\nThis skill is a dispatcher: identify the task type, load the matching workflow prompt/skill file, and follow it directly. Keep responses concise and ask a clarifying question if the correct prompt is unclear.\n\nRead only the files you need:\nLoad these files from `github/gh-aw` (they are not available locally).\n- `.github/aw/agentic-chat.md`\n- `.github/aw/agentic-workflows-mcp.md`\n- `.github/aw/asciicharts.md`\n- `.github/aw/campaign.md`\n- `.github/aw/charts-trending.md`\n- `.github/aw/charts.md`\n- `.github/aw/cli-commands.md`\n- `.github/aw/context.md`\n- `.github/aw/create-agentic-workflow.md`\n- `.github/aw/create-shared-agentic-workflow.md`\n- `.github/aw/debug-agentic-workflow.md`\n- `.github/aw/dependabot.md`\n- `.github/aw/deployment-status.md`\n- `.github/aw/experiments.md`\n- `.github/aw/github-agentic-workflows.md`\n- `.github/aw/github-mcp-server.md`\n- `.github/aw/llms.md`\n- `.github/aw/mcp-clis.md`\n- `.github/aw/memory.md`\n- `.github/aw/messages.md`\n- `.github/aw/network.md`\n- `.github/aw/optimize-agentic-workflow.md`\n- `.github/aw/patterns.md`\n- `.github/aw/pr-reviewer.md`\n- `.github/aw/report.md`\n- `.github/aw/reuse.md`\n- `.github/aw/safe-outputs-automation.md`\n- `.github/aw/safe-outputs-content.md`\n- `.github/aw/safe-outputs-management.md`\n- `.github/aw/safe-outputs-runtime.md`\n- `.github/aw/safe-outputs.md`\n- `.github/aw/serena-tool.md`\n- `.github/aw/shared-safe-jobs.md`\n- `.github/aw/skills.md`\n- `.github/aw/subagents.md`\n- `.github/aw/syntax-agentic.md`\n- `.github/aw/syntax-core.md`\n- `.github/aw/syntax-tools-imports.md`\n- `.github/aw/syntax.md`\n- `.github/aw/test-coverage.md`\n- `.github/aw/test-expression.md`\n- `.github/aw/token-optimization.md`\n- `.github/aw/triggers.md`\n- `.github/aw/update-agentic-workflow.md`\n- `.github/aw/upgrade-agentic-workflows.md`\n- `.github/aw/visual-regression.md`\n- `.github/aw/workflow-constraints.md`\n- `.github/aw/workflow-editing.md`\n- `.github/aw/workflow-patterns.md`\n\n- `.github/skills/agentic-workflow-designer/SKILL.md`\nAfter loading the matching workflow prompt or skill, follow it directly:\n- Design workflows from scratch via interview: `skills/agentic-workflow-designer/SKILL.md`\n- Create new workflows: `.github/aw/create-agentic-workflow.md`\n- Update existing workflows: `.github/aw/update-agentic-workflow.md`\n- Debug, audit, or investigate workflows: `.github/aw/debug-agentic-workflow.md`\n- Upgrade workflows and fix deprecations: `.github/aw/upgrade-agentic-workflows.md`\n- Create shared components or MCP wrappers: `.github/aw/create-shared-agentic-workflow.md`\n- Create report-generating workflows: `.github/aw/report.md`\n- Fix Dependabot manifest PRs: `.github/aw/dependabot.md`\n- Analyze coverage workflows: `.github/aw/test-coverage.md`\n- Render compact markdown charts: `.github/aw/asciicharts.md`\n- Map CLI commands to MCP usage: `.github/aw/cli-commands.md`\n- Choose workflow architecture and patterns: `.github/aw/patterns.md`\n- Optimize token usage and cost: `.github/aw/token-optimization.md`\n\nWhen 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 or skill.\n",".github/skills/benchmark/SKILL.md":"---\nname: benchmark\ndescription: Measure Z3 performance on a formula or file. Collects wall-clock time, theory solver statistics, memory usage, and conflict counts. Results are logged to z3agent.db for longitudinal tracking.\n---\n\nGiven an SMT-LIB2 formula or file, run Z3 with statistics enabled and report performance characteristics. This is useful for identifying performance regressions, comparing tactic strategies, and profiling theory solver workload distribution.\n\n# Step 1: Run Z3 with statistics\n\nAction:\n    Invoke benchmark.py with the formula or file. Use `--runs N` for\n    repeated timing.\n\nExpectation:\n    The script invokes `z3 -st`, parses the statistics block, and prints\n    a performance summary. A run entry is logged to z3agent.db.\n\nResult:\n    Timing and statistics are displayed. Proceed to Step 2 to interpret.\n\n```bash\npython3 scripts/benchmark.py --file problem.smt2\npython3 scripts/benchmark.py --file problem.smt2 --runs 5\npython3 scripts/benchmark.py --formula \"(declare-const x Int)...\" --debug\n```\n\n# Step 2: Interpret the output\n\nAction:\n    Review wall-clock time, memory usage, conflict counts, and per-theory\n    breakdowns.\n\nExpectation:\n    A complete performance profile including min/median/max timing when\n    multiple runs are requested.\n\nResult:\n    If performance is acceptable, no action needed.\n    If slow, try **simplify** to reduce the formula or adjust tactic strategies.\n\nThe output includes:\n\n- wall-clock time (ms)\n- result (sat/unsat/unknown/timeout)\n- memory usage (MB)\n- conflicts, decisions, propagations\n- per-theory breakdown (arithmetic, bv, array, etc.)\n\nWith `--runs N`, the script runs Z3 N times and reports min/median/max timing.\n\n# Step 3: Compare over time\n\nAction:\n    Query past benchmark runs from z3agent.db to detect regressions or\n    improvements.\n\nExpectation:\n    Historical run data is available for comparison, ordered by recency.\n\nResult:\n    If performance regressed, investigate recent formula or tactic changes.\n    If improved, record the successful configuration.\n\n```bash\npython3 ../../shared/z3db.py runs --skill benchmark --last 20\npython3 ../../shared/z3db.py query \"SELECT smtlib2, result, stats FROM formulas WHERE run_id IN (SELECT run_id FROM runs WHERE skill='benchmark') ORDER BY run_id DESC LIMIT 5\"\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula |\n| file | path | no | | path to .smt2 file |\n| runs | int | no | 1 | number of repeated runs for timing |\n| timeout | int | no | 60 | seconds per run |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/encode/SKILL.md":"---\nname: encode\ndescription: Translate constraint problems into SMT-LIB2 or Z3 Python API code. Handles common problem classes including scheduling, graph coloring, arithmetic puzzles, and verification conditions.\n---\n\nGiven a problem description (natural language, pseudocode, or a partial formulation), produce a complete, syntactically valid SMT-LIB2 encoding or Z3 Python script. The encoding should declare all variables, assert all constraints, and include the appropriate check-sat / get-model commands.\n\n# Step 1: Identify the problem class\n\nAction:\n    Determine the SMT theory and variable sorts required by the problem\n    description.\n\nExpectation:\n    A clear mapping from the problem to one of the supported theories\n    (LIA, LRA, QF_BV, etc.).\n\nResult:\n    If the theory is identified, proceed to Step 2. If the problem spans\n    multiple theories, select the appropriate combined logic.\n\n| Problem class | Theory | Typical sorts |\n|---------------|--------|---------------|\n| Integer arithmetic | LIA / NIA | Int |\n| Real arithmetic | LRA / NRA | Real |\n| Bitvector operations | QF_BV | (_ BitVec N) |\n| Arrays and maps | QF_AX | (Array Int Int) |\n| Strings and regex | QF_S | String, RegLan |\n| Uninterpreted functions | QF_UF | custom sorts |\n| Mixed theories | AUFLIA, etc. | combination |\n\n# Step 2: Generate the encoding\n\nAction:\n    Invoke encode.py with the problem description and desired output format.\n\nExpectation:\n    The script produces a complete SMT-LIB2 file or Z3 Python script with\n    all declarations, constraints, and check-sat commands.\n\nResult:\n    For `smtlib2` format: pass the output to **solve**.\n    For `python` format: execute the script directly.\n    Proceed to Step 3 for validation.\n\n```bash\npython3 scripts/encode.py --problem \"Find integers x, y such that x^2 + y^2 = 25 and x > 0\" --format smtlib2\npython3 scripts/encode.py --problem \"Schedule 4 tasks on 2 machines minimizing makespan\" --format python\n```\n\n# Step 3: Validate the encoding\n\nAction:\n    The script runs a syntax check by piping the output through `z3 -in`\n    in parse-only mode.\n\nExpectation:\n    No parse errors. If errors occur, the offending line is reported.\n\nResult:\n    On success: the encoding is ready for **solve**, **prove**, or **optimize**.\n    On parse error: fix the reported line and re-run.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| problem | string | yes | | problem description |\n| format | string | no | smtlib2 | output format: smtlib2 or python |\n| output | path | no | stdout | write to file instead of stdout |\n| validate | flag | no | on | run syntax check on the output |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/explain/SKILL.md":"---\nname: explain\ndescription: Parse and interpret Z3 output for human consumption. Handles models, unsat cores, proofs, statistics, and error messages. Translates solver internals into plain-language explanations.\n---\n\nGiven raw Z3 output (from the **solve**, **prove**, **optimize**, or **benchmark** skills), produce a structured explanation. This skill is for cases where the solver output is large, nested, or otherwise difficult to read directly.\n\n# Step 1: Identify the output type\n\nAction:\n    Determine the category of Z3 output to explain: model, core,\n    statistics, error, or proof.\n\nExpectation:\n    The output type maps to one of the recognized formats in the table below.\n\nResult:\n    If the type is ambiguous, use `--type auto` and let the script detect it.\n    Proceed to Step 2.\n\n| Output contains | Explanation type |\n|----------------|-----------------|\n| `(define-fun ...)` blocks | model explanation |\n| unsat core labels | conflict explanation |\n| `:key value` statistics | performance breakdown |\n| `(error ...)` | error diagnosis |\n| proof terms | proof sketch |\n\n# Step 2: Run the explainer\n\nAction:\n    Invoke explain.py with the output file or stdin.\n\nExpectation:\n    The script auto-detects the output type and produces a structured\n    plain-language summary.\n\nResult:\n    A formatted explanation is printed. If detection fails, re-run with\n    an explicit `--type` flag.\n\n```bash\npython3 scripts/explain.py --file output.txt\npython3 scripts/explain.py --stdin < output.txt\npython3 scripts/explain.py --file output.txt --debug\n```\n\n# Step 3: Interpret the explanation\n\nAction:\n    Review the structured explanation for accuracy and completeness.\n\nExpectation:\n    Models list each variable with its value and sort. Cores list\n    conflicting assertions. Statistics show time and memory breakdowns.\n\nResult:\n    Use the explanation to answer the user query or to guide the next\n    skill invocation.\n\nFor models:\n- Each variable is listed with its value and sort\n- Array and function interpretations are expanded\n- Bitvector values are shown in decimal and hex\n\nFor unsat cores:\n- The conflicting named assertions are listed\n- A minimal conflict set is highlighted\n\nFor statistics:\n- Time breakdown by phase (preprocessing, solving, model construction)\n- Theory solver load distribution\n- Memory high-water mark\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| file | path | no | | file containing Z3 output |\n| stdin | flag | no | off | read from stdin |\n| type | string | no | auto | force output type: model, core, stats, error |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/memory-safety/SKILL.md":"---\nname: memory-safety\ndescription: Run AddressSanitizer and UndefinedBehaviorSanitizer on the Z3 test suite to detect memory errors, undefined behavior, and leaks. Logs each finding to z3agent.db.\n---\n\nBuild Z3 with compiler-based sanitizer instrumentation, execute the test suite, and parse the runtime output for memory safety violations. Supported sanitizers are AddressSanitizer (heap and stack buffer overflows, use-after-free, double-free, memory leaks) and UndefinedBehaviorSanitizer (signed integer overflow, null pointer dereference, misaligned access, shift errors). Findings are deduplicated and stored in z3agent.db for triage and longitudinal tracking.\n\n# Step 1: Configure and build\n\nAction:\n    Invoke the script with the desired sanitizer flag. The script calls\n    cmake with the appropriate `-fsanitize` flags and builds the `test-z3`\n    target. Each sanitizer uses a separate build directory to avoid flag\n    conflicts.\n\nExpectation:\n    cmake configures successfully and make compiles the instrumented binary.\n    If a prior build exists with matching flags, only incremental compilation\n    runs.\n\nResult:\n    On success: an instrumented `test-z3` binary is ready in the build\n    directory. Proceed to Step 2.\n    On failure: verify compiler support for the requested sanitizer flags\n    and review cmake output.\n\n```bash\npython3 scripts/memory_safety.py --sanitizer asan\npython3 scripts/memory_safety.py --sanitizer ubsan\npython3 scripts/memory_safety.py --sanitizer both\n```\n\nTo reuse an existing build:\n```bash\npython3 scripts/memory_safety.py --sanitizer asan --skip-build --build-dir build/sanitizer-asan\n```\n\n# Step 2: Run and collect\n\nAction:\n    Execute the instrumented test binary with halt_on_error=0 so all\n    violations are reported rather than aborting on the first.\n\nExpectation:\n    The script parses AddressSanitizer, UndefinedBehaviorSanitizer, and\n    LeakSanitizer patterns from combined output, extracts source locations,\n    and deduplicates by category/file/line.\n\nResult:\n    On `clean`: no violations detected.\n    On `findings`: one or more violations found, each printed with severity,\n    category, message, and source location.\n    On `timeout`: test suite did not finish; increase timeout or investigate.\n    On `error`: build or execution failed before sanitizer output.\n\n```bash\npython3 scripts/memory_safety.py --sanitizer asan --timeout 900 --debug\n```\n\n# Step 3: Interpret results\n\nAction:\n    Review printed findings and query z3agent.db for historical comparison.\n\nExpectation:\n    Each finding includes severity, category, message, and source location.\n    The database query returns prior runs for trend analysis.\n\nResult:\n    On `clean`: no action required; proceed.\n    On `findings`: triage by severity and category. Compare against prior\n    runs to distinguish new regressions from known issues.\n    On `timeout`: increase the deadline or investigate a possible infinite\n    loop.\n    On `error`: inspect build logs before re-running.\n\nQuery past runs:\n```bash\npython3 ../../shared/z3db.py runs --skill memory-safety --last 10\npython3 ../../shared/z3db.py query \"SELECT category, severity, file, line, message FROM findings WHERE run_id IN (SELECT run_id FROM runs WHERE skill='memory-safety') ORDER BY run_id DESC LIMIT 20\"\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| sanitizer | choice | no | asan | which sanitizer to enable: asan, ubsan, or both |\n| build-dir | path | no | build/sanitizer-{name} | path to the build directory |\n| timeout | int | no | 600 | seconds before killing the test run |\n| skip-build | flag | no | off | reuse an existing instrumented build |\n| debug | flag | no | off | verbose cmake, make, and test output |\n| db | path | no | .z3-agent/z3agent.db | path to the logging database |\n",".github/skills/optimize/SKILL.md":"---\nname: optimize\ndescription: Solve constrained optimization problems using Z3. Supports minimization and maximization of objective functions over integer, real, and bitvector domains.\n---\n\nGiven a set of constraints and an objective function, find the optimal value. Z3 supports both hard constraints (must hold) and soft constraints (weighted preferences), as well as lexicographic multi-objective optimization.\n\n# Step 1: Formulate the problem\n\nAction:\n    Write constraints and an objective using `(minimize ...)` or\n    `(maximize ...)` directives, followed by `(check-sat)` and `(get-model)`.\n\nExpectation:\n    A valid SMT-LIB2 formula with at least one optimization directive and\n    all variables declared.\n\nResult:\n    If the formula is well-formed, proceed to Step 2. For multi-objective\n    problems, list directives in priority order for lexicographic optimization.\n\nExample: minimize `x + y` subject to `x >= 1`, `y >= 2`, `x + y <= 10`:\n```smtlib\n(declare-const x Int)\n(declare-const y Int)\n(assert (>= x 1))\n(assert (>= y 2))\n(assert (<= (+ x y) 10))\n(minimize (+ x y))\n(check-sat)\n(get-model)\n```\n\n# Step 2: Run the optimizer\n\nAction:\n    Invoke optimize.py with the formula or file path.\n\nExpectation:\n    The script prints `sat` with the optimal assignment, `unsat`, `unknown`,\n    or `timeout`. A run entry is logged to z3agent.db.\n\nResult:\n    On `sat`: proceed to Step 3 to read the optimal values.\n    On `unsat` or `timeout`: check constraints for contradictions or simplify.\n\n```bash\npython3 scripts/optimize.py --file scheduling.smt2\npython3 scripts/optimize.py --formula \"<inline smt-lib2>\" --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Parse the objective value and satisfying assignment from the output.\n\nExpectation:\n    `sat` with a model containing the optimal value, `unsat` indicating\n    infeasibility, or `unknown`/`timeout`.\n\nResult:\n    On `sat`: report the optimal value and assignment.\n    On `unsat`: the constraints are contradictory, no feasible solution exists.\n    On `unknown`/`timeout`: relax constraints or try **simplify**.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula with minimize/maximize |\n| file | path | no | | path to .smt2 file |\n| timeout | int | no | 60 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/prove/SKILL.md":"---\nname: prove\ndescription: Prove validity of logical statements by negation and satisfiability checking. If the negation is unsatisfiable, the original statement is valid. Otherwise a counterexample is returned.\n---\n\nGiven a conjecture (an SMT-LIB2 assertion or a natural language claim), determine whether it holds universally. The method is standard: negate the conjecture and check satisfiability. If the negation is unsatisfiable, the original is valid. If satisfiable, the model is a counterexample.\n\n# Step 1: Prepare the negated formula\n\nAction:\n    Wrap the conjecture in `(assert (not ...))` and append\n    `(check-sat)(get-model)`.\n\nExpectation:\n    A complete SMT-LIB2 formula that negates the original conjecture with\n    all variables declared.\n\nResult:\n    If the negation is well-formed, proceed to Step 2.\n    If the conjecture is natural language, run **encode** first.\n\nExample: to prove that `(> x 3)` implies `(> x 1)`:\n```smtlib\n(declare-const x Int)\n(assert (not (=> (> x 3) (> x 1))))\n(check-sat)\n(get-model)\n```\n\n# Step 2: Run the prover\n\nAction:\n    Invoke prove.py with the conjecture and variable declarations.\n\nExpectation:\n    The script prints `valid`, `invalid` (with counterexample), `unknown`,\n    or `timeout`. A run entry is logged to z3agent.db.\n\nResult:\n    On `valid`: proceed to **explain** if the user needs a summary.\n    On `invalid`: report the counterexample directly.\n    On `unknown`/`timeout`: try **simplify** first, or increase the timeout.\n\n```bash\npython3 scripts/prove.py --conjecture \"(=> (> x 3) (> x 1))\" --vars \"x:Int\"\n```\n\nFor file input where the file contains the full negated formula:\n```bash\npython3 scripts/prove.py --file negated.smt2\n```\n\nWith debug tracing:\n```bash\npython3 scripts/prove.py --conjecture \"(=> (> x 3) (> x 1))\" --vars \"x:Int\" --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Read the prover output to determine validity of the conjecture.\n\nExpectation:\n    One of `valid`, `invalid` (with counterexample), `unknown`, or `timeout`.\n\nResult:\n    On `valid`: the conjecture holds universally.\n    On `invalid`: the model shows a concrete counterexample.\n    On `unknown`/`timeout`: the conjecture may require auxiliary lemmas or induction.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| conjecture | string | no | | the assertion to prove (without negation) |\n| vars | string | no | | variable declarations as \"name:sort\" pairs, comma-separated |\n| file | path | no | | .smt2 file with the negated formula |\n| timeout | int | no | 30 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\nEither `conjecture` (with `vars`) or `file` must be provided.\n",".github/skills/simplify/SKILL.md":"---\nname: simplify\ndescription: Reduce formula complexity using Z3 tactic chains. Supports configurable tactic pipelines for boolean, arithmetic, and bitvector simplification.\n---\n\nGiven a formula, apply a sequence of Z3 tactics to produce an equivalent but simpler form. This is useful for understanding what Z3 sees after preprocessing, debugging tactic selection, and reducing formula size before solving.\n\n# Step 1: Choose tactics\n\nAction:\n    Select a tactic chain from the available Z3 tactics based on the\n    formula's theory.\n\nExpectation:\n    A comma-separated list of tactic names suitable for the formula domain.\n\nResult:\n    If unsure, use the default chain: `simplify,propagate-values,ctx-simplify`.\n    For bitvector formulas, add `bit-blast`. Proceed to Step 2.\n\n| Tactic | What it does |\n|--------|-------------|\n| simplify | constant folding, algebraic identities |\n| propagate-values | substitute known equalities |\n| ctx-simplify | context-dependent simplification |\n| elim-uncnstr | remove unconstrained variables |\n| solve-eqs | Gaussian elimination |\n| bit-blast | reduce bitvectors to booleans |\n| tseitin-cnf | convert to CNF |\n| aig | and-inverter graph reduction |\n\n# Step 2: Run simplification\n\nAction:\n    Invoke simplify.py with the formula and optional tactic chain.\n\nExpectation:\n    The script applies each tactic in sequence and prints the simplified\n    formula. A run entry is logged to z3agent.db.\n\nResult:\n    If the output is simpler, pass it to **solve** or **prove**.\n    If unchanged, try a different tactic chain.\n\n```bash\npython3 scripts/simplify.py --formula \"(assert (and (> x 0) (> x 0)))\" --vars \"x:Int\"\npython3 scripts/simplify.py --file formula.smt2 --tactics \"simplify,propagate-values,ctx-simplify\"\npython3 scripts/simplify.py --file formula.smt2 --debug\n```\n\nWithout `--tactics`, the script applies the default chain: `simplify`, `propagate-values`, `ctx-simplify`.\n\n# Step 3: Interpret the output\n\nAction:\n    Read the simplified formula output in SMT-LIB2 syntax.\n\nExpectation:\n    One or more `(assert ...)` blocks representing equivalent subgoals.\n\nResult:\n    A smaller formula indicates successful reduction. Pass the result to\n    **solve**, **prove**, or **optimize** as needed.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula to simplify |\n| vars | string | no | | variable declarations as \"name:sort\" pairs |\n| file | path | no | | path to .smt2 file |\n| tactics | string | no | simplify,propagate-values,ctx-simplify | comma-separated tactic names |\n| timeout | int | no | 30 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/solve/SKILL.md":"---\nname: solve\ndescription: Check satisfiability of SMT-LIB2 formulas using Z3. Returns sat/unsat with models or unsat cores. Logs every invocation to z3agent.db for auditability.\n---\n\nGiven an SMT-LIB2 formula (or a set of constraints described in natural language), determine whether the formula is satisfiable. If sat, extract a satisfying assignment. If unsat and tracking labels are present, extract the unsat core.\n\n# Step 1: Prepare the formula\n\nAction:\n    Convert the input to valid SMT-LIB2. If the input is natural language,\n    use the **encode** skill first.\n\nExpectation:\n    A syntactically valid SMT-LIB2 formula ending with `(check-sat)` and\n    either `(get-model)` or `(get-unsat-core)` as appropriate.\n\nResult:\n    If valid SMT-LIB2 is ready, proceed to Step 2.\n    If encoding is needed, run **encode** first and return here.\n\n# Step 2: Run Z3\n\nAction:\n    Invoke solve.py with the formula string or file path.\n\nExpectation:\n    The script pipes the formula to `z3 -in`, logs the run to\n    `.z3-agent/z3agent.db`, and prints the result.\n\nResult:\n    Output is one of `sat`, `unsat`, `unknown`, or `timeout`.\n    Proceed to Step 3 to interpret.\n\n```bash\npython3 scripts/solve.py --formula \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\"\n```\n\nFor file input:\n```bash\npython3 scripts/solve.py --file problem.smt2\n```\n\nWith debug tracing:\n```bash\npython3 scripts/solve.py --file problem.smt2 --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Parse the Z3 output to determine satisfiability and extract any model\n    or unsat core.\n\nExpectation:\n    `sat` with a model, `unsat` optionally with a core, `unknown`, or\n    `timeout`.\n\nResult:\n    On `sat`: report the model to the user.\n    On `unsat`: report the core if available.\n    On `unknown`/`timeout`: try **simplify** or increase the timeout.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula as a string |\n| file | path | no | | path to an .smt2 file |\n| timeout | int | no | 30 | seconds before killing z3 |\n| z3 | path | no | auto | explicit path to z3 binary |\n| debug | flag | no | off | print z3 command, stdin, stdout, stderr, timing |\n| db | path | no | .z3-agent/z3agent.db | path to the logging database |\n\nEither `formula` or `file` must be provided.\n",".github/skills/static-analysis/SKILL.md":"---\nname: static-analysis\ndescription: Run Clang Static Analyzer (scan-build) on Z3 source and log structured findings to z3agent.db.\n---\n\nRun the Clang Static Analyzer over a CMake build of Z3, parse the resulting plist diagnostics, and record each finding with file, line, category, and description. This skill wraps scan-build into a reproducible, logged workflow suitable for regular analysis sweeps and regression tracking.\n\n# Step 1: Run the analysis\n\nAction:\n    Invoke the script pointing at the CMake build directory. The script\n    runs `scan-build cmake -S . -B <build-dir>` followed by a scan-build-wrapped\n    `cmake --build` and writes\n    checker output to the output directory.\n\nExpectation:\n    scan-build completes within the timeout, producing plist diagnostic\n    files in the output directory (defaults to a `scan-results` subdirectory\n    of the build directory).\n\nResult:\n    On success: diagnostics are parsed and findings are printed. Proceed to\n    Step 2.\n    On failure: verify that clang and scan-build are installed and that the\n    build directory contains a valid CMake configuration.\n\n```bash\npython3 scripts/static_analysis.py --build-dir build\npython3 scripts/static_analysis.py --build-dir build --output-dir /tmp/sa-results --debug\npython3 scripts/static_analysis.py --build-dir build --timeout 1800\n```\n\n# Step 2: Interpret the output\n\nAction:\n    Review the printed findings and the summary table grouped by category.\n\nExpectation:\n    Each finding shows its source location, category, and description.\n    The summary table ranks categories by frequency for quick triage.\n\nResult:\n    On zero findings: the codebase passes all enabled static checks.\n    On findings: prioritize by category frequency and severity. Address\n    null dereferences and use-after-free classes first.\n\nExample output:\n\n```\n[Dead store] src/ast/ast.cpp:142: Value stored to 'result' is never read\n[Null dereference] src/smt/theory_lra.cpp:87: Access to field 'next' results in a dereference of a null pointer\n```\n\n# Step 3: Review historical findings\n\nAction:\n    Query z3agent.db to compare current results against prior analysis\n    runs.\n\nExpectation:\n    Queries return category counts and run history, enabling regression\n    detection across commits.\n\nResult:\n    On stable or decreasing counts: no regressions introduced.\n    On increased counts: cross-reference new findings with recent commits\n    to identify the responsible change.\n\n```bash\npython3 ../../shared/z3db.py query \"SELECT category, COUNT(*) as cnt FROM findings WHERE run_id IN (SELECT run_id FROM runs WHERE skill='static-analysis') GROUP BY category ORDER BY cnt DESC\"\npython3 ../../shared/z3db.py runs --skill static-analysis --last 10\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| build-dir | path | yes | | path to the CMake build directory |\n| output-dir | path | no | BUILD/scan-results | directory for scan-build output |\n| timeout | int | no | 1200 | seconds allowed for the full build |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n| debug | flag | no | off | verbose tracing |\n"},"files":{".github/copilot-instructions.md":"# Z3 Theorem Prover Development Guide\n\nAlways reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here.\n\n## Working Effectively\n\n### Bootstrap and Build the Repository\n\nZ3 is built with CMake:\n- `cmake -S . -B build` -- takes 1 second to configure\n- `cmake --build build --parallel $(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Dependencies and Requirements\n- Python 3.x (required to run CMake's code generation scripts)\n- C++20 capable compiler (g++ or clang++)\n- Git (for version information)\n\n### Test the Repository\n\n- Build unit tests: `cmake --build build --target test-z3 --parallel $(nproc)` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**Test basic Z3 functionality:**\n```bash\n./z3 --version\necho \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\" | ./z3 -in\n```\n\n### Validation Scenarios\n\n**ALWAYS** test these scenarios after making changes:\n\n#### Basic SMT Solving\n```bash\ncd build\necho \"(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(get-model)\" | ./z3 -in\n```\nExpected output: `sat` followed by a model showing `x = 1` or similar.\n\n#### Python Bindings\n```bash\ncd build/python\npython3 -c \"import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())\"\n```\nExpected output: `Result: sat` and `Model: [x = 1]` or similar.\n\n#### Command Line Help\n```bash\n./z3 --help | head -10\n```\nShould display version and usage information.\n\n## Build System Details\n\n### CMake Build System\n- Configuration: `cmake -S . -B build` (1 second)\n- Main build: `cmake --build build --parallel $(nproc)` (17 minutes)\n- Creates Python bindings in `build/python/` when `-DZ3_BUILD_PYTHON_BINDINGS=ON` is set\n- Out-of-source build: clean build tree, no source pollution\n\n### Critical Timing and Timeout Requirements\n\n**NEVER CANCEL these operations**:\n- `cmake --build build --parallel $(nproc)`: 15-17 minutes. **Set timeout to 30+ minutes minimum**.\n- `cmake --build build --target test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**.\n- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**.\n\n**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing.\n\n## Repository Structure\n\n### Key Directories\n- `src/` - Main source code organized by components (ast, smt, sat, etc.)\n- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.)\n- `scripts/` - Build scripts and utilities\n- `.github/workflows/` - CI/CD pipeline definitions\n- `cmake/` - CMake configuration files\n\n### Important Files\n- `README.md` - Main documentation and build instructions\n- `README-CMake.md` - Detailed CMake build documentation\n- `CMakeLists.txt` - Main CMake configuration\n\n## Common Tasks and Validation\n\n### Pre-commit Validation\nBefore committing changes:\n1. **Build successfully**: Use one of the validated build commands above\n2. **Run unit tests**: `./test-z3 /a` must pass\n3. **Test basic functionality**: Run validation scenarios above\n4. **Test affected language bindings**: If modifying API, test relevant examples\n\n### Working with Language Bindings\n- **Python**: Located in `build/python/`, test with validation scenario above\n- **C/C++**: Examples in `examples/c/` and `examples/c++/`\n  - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example`\n  - Run with: `LD_LIBRARY_PATH=build ./test_example`\n- **Java**: Build with `cmake -S . -B build -DZ3_BUILD_JAVA_BINDINGS=ON`, examples in `examples/java/`\n- **C#/.NET**: Build with `cmake -S . -B build -DZ3_BUILD_DOTNET_BINDINGS=ON`, examples in `examples/dotnet/`\n\n### Performance Testing\nFor performance-sensitive changes:\n- Build optimized: `cmake -S . -B build -DCMAKE_BUILD_TYPE=Release` (Release mode)\n- Test with realistic SMT problems from `examples/SMT-LIB2/`\n- Use Z3's built-in statistics: `z3 -st problem.smt2`\n\n## Common Issues and Solutions\n\n### Python Import Errors\n- **Error**: `import z3` fails\n- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH`\n\n### Missing Dependencies\n- **Error**: Compiler not found or version too old\n- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+\n\n### Long Build Times\n- **Normal**: 15-17 minute builds are expected for Z3\n- **Never cancel**: Set timeouts appropriately and wait for completion\n- **Optimization**: Use `cmake --build build --parallel $(nproc)` for parallel compilation\n\n## Key Projects in Codebase\n\nZ3 is organized into several key components:\n\n- **Core SMT**: `src/smt/` - Main SMT solver engine\n- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver  \n- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.)\n- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation\n- **Tactics**: `src/tactic/` - Configurable solving strategies\n- **API**: `src/api/` - Public C API and language bindings\n- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers\n- **Model Generation**: Creating and manipulating satisfying assignments\n\nThe architecture is modular with clean separation between the core solver, theory plugins, and user interfaces.\n",".github/skills/README.md":"# Z3 Agent Skills\n\nReusable, composable verification primitives for the Z3 theorem prover.\nEach skill is a self-contained unit: a `SKILL.md` prompt that guides the\nLLM agent, backed by a Python validation script in `scripts/`.\n\n## Skill Catalogue\n\n| Skill | Status | Description |\n|-------|--------|-------------|\n| solve | implemented | Check satisfiability of SMT-LIB2 formulas; return models or unsat cores |\n| prove | implemented | Prove validity by negation and satisfiability checking |\n| encode | implemented | Translate constraint problems into SMT-LIB2 or Z3 Python API code |\n| simplify | implemented | Reduce formula complexity using configurable Z3 tactic chains |\n| optimize | implemented | Solve constrained optimization (minimize/maximize) over numeric domains |\n| explain | implemented | Parse and interpret Z3 output: models, cores, statistics, errors |\n| benchmark | implemented | Measure Z3 performance and collect solver statistics |\n| static-analysis | implemented | Run Clang Static Analyzer on Z3 source and log structured findings |\n| memory-safety | implemented | Run ASan/UBSan on Z3 test suite to detect memory errors and undefined behavior |\n\n## Agent\n\nA single orchestration agent composes these skills into end-to-end workflows:\n\n| Agent | Role |\n|-------|------|\n| z3 | SMT solving, code quality analysis, and stress testing |\n\n## Shared Infrastructure\n\nAll scripts share a common library at `shared/z3db.py` with:\n\n* `Z3DB`: SQLite wrapper for tracking runs, formulas, findings, and interaction logs.\n* `run_z3()`: Pipe SMT-LIB2 into `z3 -in` with timeout handling.\n* `find_z3()`: Locate the Z3 binary across build directories and PATH.\n* Parsers: `parse_model()`, `parse_stats()`, `parse_unsat_core()`.\n\nThe database schema lives in `shared/schema.sql`.\n\n## Relationship to a3/ Workflows\n\nThe `a3/` directory at the repository root contains two existing agentic workflow\nprompts that predate the skill architecture:\n\n* `a3/a3-python.md`: A3 Python Code Analysis agent (uses the a3-python pip tool\n  to scan Python source, classifies findings, creates GitHub issues).\n* `a3/a3-rust.md`: A3 Rust Verifier Output Analyzer (downloads a3-rust build\n  artifacts, parses bug reports, creates GitHub discussions).\n\nThese workflows are complementary to the skills defined here, not replaced by\nthem. The a3 prompts focus on external analysis tooling and GitHub integration,\nwhile skills focus on Z3 solver operations and their validation. Both may be\ncomposed by the same orchestrating agent.\n\n## Usage\n\nCheck database status and recent runs:\n\n```\npython shared/z3db.py status\npython shared/z3db.py runs --skill solve --last 5\npython shared/z3db.py log --run-id 12\npython shared/z3db.py query \"SELECT skill, COUNT(*) FROM runs GROUP BY skill\"\n```\n\nRun an individual skill script directly:\n\n```\npython solve/scripts/solve.py --file problem.smt2\npython encode/scripts/encode.py --validate formula.smt2\npython benchmark/scripts/benchmark.py --file problem.smt2\n```\n",".github/skills/agentic-workflow-designer/SKILL.md":"---\nname: agentic-workflow-designer\ndescription: Conversational skill that interviews users to design new agentic workflows\ndisable-model-invocation: true\n---\n\n# Workflow Designer\n\nUse this skill to run a structured interview with users who know their goal but not the workflow syntax yet, then generate one complete workflow `.md` file.\n\n## When to Use This Skill\n\nUse this before `.github/aw/create-agentic-workflow.md` when requirements are unclear or incomplete.\n\n- Use `skills/agentic-workflow-designer/SKILL.md` to discover and confirm requirements.\n- Use `.github/aw/create-agentic-workflow.md` once requirements are clear and ready for implementation.\n- Use `.github/aw/agentic-chat.md` when the user wants a specification/pseudo-code instead of a runnable workflow file.\n\n## Interview Framework\n\nAsk one question at a time. Move to the next phase only after the current phase is clear.\n\n### Phase 1: Goal\n\nAsk: **\"What do you want to automate?\"**\n\nCapture:\n- Workflow name (kebab-case candidate)\n- Brief description\n- Optional emoji\n\n### Phase 2: Trigger\n\nAsk: **\"When should this run?\"**\n\nFollow up only if needed:\n- Which event type(s)?\n- Any filters (labels, branches, commands)?\n- Scheduled cadence (daily/weekly/hourly)?\n\nMap to the `on:` block.\n\n### Phase 3: Scope (Read/Write)\n\nAsk:\n- **\"What should it read?\"** (issues, PRs, code, discussions, CI data)\n- **\"What should it create or update?\"** (comments, issues, PRs, labels)\n\nMap to:\n- `permissions:` (keep read-only for agent job)\n- `tools:`\n- `safe-outputs:`\n\n### Phase 4: Data Strategy\n\nAsk:\n- **\"What data does the agent need to make decisions?\"**\n- Follow up: **\"Can we pre-fetch and aggregate that data with shell commands so the agent only reads compact JSON?\"**\n\nCapture:\n- Whether `steps:` should pre-fetch GitHub data with `gh` + `jq`\n- Output paths under `/tmp/gh-aw/data/`\n- Whether batch work should use sub-agents\n\nMap to:\n- `steps:`\n- Prompt references to pre-computed file paths\n\n### Phase 5: Guardrails\n\nAsk: **\"Should it block merging, just advise, or silently log?\"**\n\nCapture:\n- Visibility expectations (comment, issue, no visible output)\n- No-op behavior expectation\n\nGuide toward safe output behavior and explicit `noop` instructions.\n\n### Phase 6: Context & Network\n\nAsk: **\"Does it need external APIs, web access, package installs, or MCP servers?\"**\n\nFollow up:\n- **\"Any third-party services or MCP servers to include (for example Slack, Jira, Datadog, custom internal MCP)?\"**\n- **\"Are you deploying on GitHub.com, GHEC with custom endpoints, or GHES?\"**\n- For each integration, identify required auth from source docs and map it to GitHub Actions secrets + workflow env variables.\n- Ask for exact external domains (FQDN/wildcard).\n\nMap to:\n- `network.allowed`\n- Optional MCP/GitHub tool usage in `tools:`\n- `secrets:` / `env:` wiring for integration tokens\n- GHES/GHEC settings such as `engine.api-target` and `aw.json` `ghes: true` (when applicable)\n\n### Phase 7: Engine (optional)\n\nAsk only if ambiguous: **\"Any AI engine preference?\"**\n\nIf no preference, suggest default:\n- \"I'd suggest Copilot since you haven't mentioned a preference. Sound good?\"\n\nMap to `engine:` only when not default.\n\n### Phase 8: Confirmation\n\nPresent a structured summary and ask for approval before generation.\n\n## Decision Heuristics\n\n### Trigger Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"when someone opens a PR\" | `on: pull_request:` with `types: [opened]` |\n| \"when a PR is updated\" | `on: pull_request:` with `types: [opened, synchronize]` |\n| \"every morning\", \"daily\" | fuzzy schedule shorthand `on: schedule: daily on weekdays` (compiler expands to cron) |\n| \"every Monday\", \"weekly\" | fuzzy schedule shorthand `on: schedule: weekly` (compiler expands to cron) |\n| \"when I say /review\" | `on: slash_command:` with `name: review` (or requested command) |\n| \"when an issue is labeled bug\" | `on: issues:` with `types: [labeled]` and label filter guidance |\n| \"run when label ai-review is added\" | `on: label_command:` with `name`/`names`, optional event scoping, and label-as-command semantics |\n| \"run on PRs from forks\" | `on: pull_request:` plus explicit `forks:` allowlist and fork security guardrails |\n| \"sometimes automatic, sometimes manual\" | semi-active pattern: combine `schedule`/event triggers with `workflow_dispatch` |\n| \"manually\", \"on demand\" | `on: workflow_dispatch:` |\n| \"when a deployment fails\" | `on: deployment_status:` |\n| \"when another workflow finishes\" | `on: workflow_run:` |\n\n### Safe Output Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"post a comment\" | `add-comment` |\n| \"create an issue\" | `create-issue` |\n| \"update issue title/body\" | `update-issue` |\n| \"close the issue\" | `close-issue` |\n| \"assign someone\", \"remove assignment\" | `assign-to-user`, `unassign-from-user` |\n| \"set issue type/field/milestone\" | `set-issue-type`, `set-issue-field`, `assign-milestone` |\n| \"open a PR\", \"submit changes\" | `create-pull-request` |\n| \"update PR description/title\" | `update-pull-request` |\n| \"close the PR\", \"merge the PR\" | `close-pull-request`, `merge-pull-request` |\n| \"mark PR ready\", \"sync PR branch\" | `mark-pull-request-as-ready-for-review`, `update-branch` |\n| \"commit a fix to the PR branch\" | `push-to-pull-request-branch` |\n| \"approve / request changes\" | `submit-pull-request-review` |\n| \"inline review comment\", \"reply to review thread\" | `create-pull-request-review-comment`, `reply-to-pull-request-review-comment`, `resolve-pull-request-review-thread` |\n| \"start or edit discussion\", \"close discussion\" | `create-discussion`, `update-discussion`, `close-discussion` |\n| \"request reviewer\", \"hide comment\" | `add-reviewer`, `hide-comment` |\n| \"create/update project\", \"project status update\" | `create-project`, `update-project`, `create-project-status-update` |\n| \"update release\", \"upload release asset\" | `update-release`, `upload-asset` |\n| \"create/auto-fix code scan alert\" | `create-code-scanning-alert`, `autofix-code-scanning-alert` |\n| \"start an agent session\", \"assign to an agent\" | `create-agent-session`, `assign-to-agent` |\n| \"store persistent memory comment\" | `comment-memory` |\n| \"link a sub-issue\" | `link-sub-issue` |\n| \"add labels\", \"remove labels\" | `add-labels`, `remove-labels` |\n| \"nothing visible\", \"just analyze\" | no safe outputs required |\n\n### Network Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"calls an external API\" | ask for exact FQDN/wildcard, then add to `network.allowed` |\n| \"reads GitHub data / clones repos\" | include `github` in `network.allowed` |\n| \"uses GitHub Actions artifacts or cache\" | include `github-actions` in `network.allowed` |\n| \"installs npm packages\" | include `node` in `network.allowed` |\n| \"runs pip install\" | include `python` in `network.allowed` |\n| \"builds Go code\" | include `go` in `network.allowed` |\n| \"installs gems / uses Bundler\" | include `ruby` in `network.allowed` |\n| \"runs cargo build\" | include `rust` in `network.allowed` |\n| \"uses NuGet / .NET restore\" | include `dotnet` in `network.allowed` |\n| \"builds with Maven / Gradle\" | include `java` in `network.allowed` |\n| \"uses Docker / pulls container images / pushes to GHCR\" | include `containers` in `network.allowed` |\n| \"runs Playwright browser tests\" | include `playwright` in `network.allowed` |\n| \"runs apt install / yum / apk\" | include `linux-distros` in `network.allowed` |\n| \"uses Terraform / HashiCorp registry\" | include `terraform` in `network.allowed` |\n| \"connects to localhost / loopback / local services\" | include `local` in `network.allowed` |\n| \"uses Swift Package Manager\" | include `swift` in `network.allowed` |\n| \"uses Composer / PHP packages\" | include `php` in `network.allowed` |\n| \"uses pub.dev / Dart packages\" | include `dart` in `network.allowed` |\n| \"uses Hackage / Haskell packages\" | include `haskell` in `network.allowed` |\n| \"uses CPAN / Perl packages\" | include `perl` in `network.allowed` |\n| \"serves or loads web fonts\" | include `fonts` in `network.allowed` |\n| \"uses Deno or JSR packages\" | include `deno` in `network.allowed` |\n| \"uses Elixir / Hex packages\" | include `elixir` in `network.allowed` |\n| \"uses Bazel build\" | include `bazel` in `network.allowed` |\n| \"uses R / CRAN packages\" | include `r` in `network.allowed` |\n| \"no external access\" | `network.allowed: [defaults]` (or `[]` if explicitly zero network) |\n\n### Tool Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"read GitHub issues/PRs/workflows\" | `tools.github` with `mode: gh-proxy` and minimal `toolsets` |\n| \"use full MCP server/tool definitions\" | `tools.github` with `mode: local` |\n| \"use other MCP servers but keep token cost down\" | `tools.cli-proxy: true` (hybrid CLI-proxy mode) |\n| \"edit files\" | `edit` tool (default unless restricted) |\n| \"run commands/tests\" | `bash` tool (default unless restricted) |\n| \"browse web pages/docs\" | `web-fetch` and/or `web-search` |\n| \"test UI flows\" | `playwright` |\n\n### Pattern Heuristics\n\n| User says... | Recommended named pattern |\n|---|---|\n| \"triage issues automatically\" | `IssueOps` |\n| \"run on /commands with human approval loops\" | `ChatOps` |\n| \"run every weekday and keep improving\" | `DailyOps` |\n| \"monitor workflow failures and trends\" | `MonitorOps` |\n| \"process a big backlog in chunks\" | `BatchOps` |\n| \"run manually with input parameters\" | `DispatchOps` |\n| \"apply a label-based workflow\" | `LabelOps` |\n| \"operate across multiple repositories\" | `MultiRepoOps` |\n| \"coordinate multiple sub-agents\" | `Orchestration` |\n| \"manage project board items\" | `ProjectOps` |\n| \"research, plan, and assign issues\" | `ResearchPlanAssignOps` |\n| \"self-correcting / retry on failure\" | `CorrectionOps` |\n| \"run in a side/fork repo\" | `SideRepoOps` |\n| \"write a spec before implementing\" | `SpecOps` |\n| \"A/B test workflow variants\" | `TrialOps` |\n| \"process items from a queue\" | `WorkQueueOps` |\n| \"deterministic, no LLM needed\" | `DeterministicOps` |\n| \"manage from a central repo\" | `CentralRepoOps` |\n| \"track work via GitHub Projects\" | `Monitoring with Projects` |\n\n### Integration Auth Mapping\n\nWhen the user names a third-party service or MCP server:\n\n1. Confirm whether native tool, MCP server, or safe-output job is the right integration path.\n2. Look up the integration's auth requirements and required scopes before finalizing the design.\n3. Provide a concrete setup checklist with:\n   - required GitHub Actions secrets (names to create)\n   - workflow env variables that consume those secrets\n   - minimum token scopes/permissions needed\n\nOutput format to use:\n\n```text\nIntegration auth setup:\n- <service-or-mcp>: <purpose>\n  - Secrets to create: <SECRET_NAME>, <SECRET_NAME>\n  - Workflow env vars: <ENV_VAR>=${{ secrets.<SECRET_NAME> }}\n  - Required scopes/permissions: <least-privilege scopes>\n```\n\nNever suggest committing plaintext tokens.\n\n### Data Strategy Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"analyze PRs\", \"review issues\", \"check status\" | add `steps:` that pre-fetch with `gh` + `jq` |\n| \"read the diff\", \"look at changed files\" | add `steps:` using `gh pr diff` or `gh pr view --json files` |\n| \"search for patterns across repos\" | add `steps:` using `gh search` + `jq` filters |\n| \"just respond to a comment\" | no pre-fetch needed (event payload is enough) |\n| \"process each item individually\" | suggest sub-agent pattern with `model: small` |\n\n## Token Optimization Defaults\n\nApply these defaults unless the user explicitly asks otherwise:\n\n1. Use DataOps by default for GitHub reads: pre-fetch/aggregate with `gh` + `jq` in `steps:`, store compact JSON in `/tmp/gh-aw/data/`, and point the prompt to those files (see `.github/aw/token-optimization.md` for details).\n2. Keep tool surface minimal: default to `tools.github.mode: gh-proxy`, include only required toolsets, and prefer `bash` + `gh` for simple reads.\n3. For batch workloads, split items into compact data and suggest sub-agent processing with `model: small`.\n4. Keep prompts compact: concise imperative instructions, explicit file paths, single-line `noop` guidance, and stable instructions before dynamic content.\n\n## Progressive Disclosure Rules\n\n1. Never dump all options at once; ask one targeted question at a time.\n2. Skip questions when answers are inferable from prior user statements.\n3. Offer smart defaults and request confirmation instead of over-questioning.\n4. Ask at most 5 questions before presenting a summary; then ask \"anything else?\" if needed.\n5. Detect done signals (`that's it`, `looks good`, `generate it`) and proceed to generation.\n\n## Confirmation Format\n\nUse this exact structure:\n\n```text\n📋 Proposed workflow:\n- Name: <workflow-id>\n- Trigger: <event + key options>\n- Engine: <engine or default>\n- Tools: <tool summary>\n- Safe outputs: <list or none>\n- Network: <allowed summary>\n- Integrations/Auth: <service/mcp + required secrets/env vars>\n- Deployment: <GitHub.com or GHEC/GHES details>\n- Intent: <one-sentence task>\n```\n\nThen ask: **\"Ready to generate, or want to adjust anything?\"**\n\n## Generation Template\n\nAfter confirmation, generate one workflow file using the same skeleton style as `.github/aw/create-agentic-workflow.md`.\n\n```markdown\n---\nemoji: <emoji>\ndescription: <brief description>\non:\n  <trigger config>\npermissions:\n  contents: read\n  issues: read\n  pull-requests: read\ntools:\n  github:\n    mode: gh-proxy\n    toolsets: [default]\nsteps:\n  - name: <optional data prefetch>\n    run: |\n      mkdir -p /tmp/gh-aw/data\n      <gh + jq commands that produce compact JSON>\nsafe-outputs:\n  <safe-output-types-if-needed>\nnetwork:\n  allowed:\n    - defaults\n    - <additional entries if needed>\n---\n\n# <Workflow Name>\n\n## Task\n\n<clear instructions tied to trigger context>\nIf `steps:` includes pre-fetch commands, read the resulting `/tmp/gh-aw/data/*.json` files instead of broad live re-fetches.\n\n## Safe Outputs\n\n- Use configured safe outputs for all visible write actions.\n- Call `noop` with a short reason when no action is needed.\n```\n\n## Validation Checklist\n\nBefore final output, run this internal self-check:\n\n- [ ] Agent job permissions remain read-only (writes only via safe outputs)\n- [ ] `safe-outputs:` covers every write action mentioned in prompt/instructions\n- [ ] Network access is scoped; avoid blanket wildcard entries\n- [ ] Trigger matches the user's intended activation event\n- [ ] Prompt instructs agent to call `noop` when no action is needed\n- [ ] Unnecessary defaults are omitted (for example `engine: copilot`)\n- [ ] If reading GitHub data, `steps:` pre-fetches compact JSON (DataOps)\n- [ ] `tools.github.mode` is `gh-proxy` unless broader MCP toolsets are explicitly needed\n- [ ] Only required toolsets are listed (avoid blanket toolset lists)\n- [ ] Prompt references specific pre-computed file paths\n- [ ] For batch processing (>5 items), sub-agent pattern is suggested\n- [ ] For each third-party service/MCP integration, required secrets/env vars are listed\n- [ ] Auth guidance includes least-privilege token scope recommendations\n- [ ] For GHEC/GHES deployments, `engine.api-target` and GHES compatibility guidance are included when needed\n\n## References (load only when needed)\n\nIn-repo references:\n- `.github/aw/syntax.md` (index → `.github/aw/syntax-core.md`, `.github/aw/syntax-agentic.md`, `.github/aw/syntax-tools-imports.md`)\n- `.github/aw/safe-outputs.md` (index → `.github/aw/safe-outputs-content.md`, `.github/aw/safe-outputs-management.md`, `.github/aw/safe-outputs-automation.md`, `.github/aw/safe-outputs-runtime.md`)\n- `.github/aw/network.md`\n- `.github/aw/patterns.md`\n- `.github/aw/subagents.md`\n- `.github/aw/token-optimization.md`\n- `.github/aw/triggers.md`\n- `.github/aw/create-agentic-workflow.md`\n\nPortable HTTPS references:\n- `https://github.com/github/gh-aw/blob/main/.github/aw/syntax.md` (index → `.../syntax-core.md`, `.../syntax-agentic.md`, `.../syntax-tools-imports.md`)\n- `https://github.com/github/gh-aw/blob/main/.github/aw/safe-outputs.md` (index → `.../safe-outputs-content.md`, `.../safe-outputs-management.md`, `.../safe-outputs-automation.md`, `.../safe-outputs-runtime.md`)\n- `https://github.com/github/gh-aw/blob/main/.github/aw/network.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/patterns.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/triggers.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/create-agentic-workflow.md`\n",".github/skills/agentic-workflows/SKILL.md":"---\nname: agentic-workflows\ndescription: Route gh-aw workflow design/create/debug/upgrade requests to the right prompts.\n---\n\n# Agentic Workflows Router\n\nUse this skill when a user asks to design, create, update, debug, or upgrade GitHub Agentic Workflows in this repository.\n\nThis skill is a dispatcher: identify the task type, load the matching workflow prompt/skill file, and follow it directly. Keep responses concise and ask a clarifying question if the correct prompt is unclear.\n\nRead only the files you need:\nLoad these files from `github/gh-aw` (they are not available locally).\n- `.github/aw/agentic-chat.md`\n- `.github/aw/agentic-workflows-mcp.md`\n- `.github/aw/asciicharts.md`\n- `.github/aw/campaign.md`\n- `.github/aw/charts-trending.md`\n- `.github/aw/charts.md`\n- `.github/aw/cli-commands.md`\n- `.github/aw/context.md`\n- `.github/aw/create-agentic-workflow.md`\n- `.github/aw/create-shared-agentic-workflow.md`\n- `.github/aw/debug-agentic-workflow.md`\n- `.github/aw/dependabot.md`\n- `.github/aw/deployment-status.md`\n- `.github/aw/experiments.md`\n- `.github/aw/github-agentic-workflows.md`\n- `.github/aw/github-mcp-server.md`\n- `.github/aw/llms.md`\n- `.github/aw/mcp-clis.md`\n- `.github/aw/memory.md`\n- `.github/aw/messages.md`\n- `.github/aw/network.md`\n- `.github/aw/optimize-agentic-workflow.md`\n- `.github/aw/patterns.md`\n- `.github/aw/pr-reviewer.md`\n- `.github/aw/report.md`\n- `.github/aw/reuse.md`\n- `.github/aw/safe-outputs-automation.md`\n- `.github/aw/safe-outputs-content.md`\n- `.github/aw/safe-outputs-management.md`\n- `.github/aw/safe-outputs-runtime.md`\n- `.github/aw/safe-outputs.md`\n- `.github/aw/serena-tool.md`\n- `.github/aw/shared-safe-jobs.md`\n- `.github/aw/skills.md`\n- `.github/aw/subagents.md`\n- `.github/aw/syntax-agentic.md`\n- `.github/aw/syntax-core.md`\n- `.github/aw/syntax-tools-imports.md`\n- `.github/aw/syntax.md`\n- `.github/aw/test-coverage.md`\n- `.github/aw/test-expression.md`\n- `.github/aw/token-optimization.md`\n- `.github/aw/triggers.md`\n- `.github/aw/update-agentic-workflow.md`\n- `.github/aw/upgrade-agentic-workflows.md`\n- `.github/aw/visual-regression.md`\n- `.github/aw/workflow-constraints.md`\n- `.github/aw/workflow-editing.md`\n- `.github/aw/workflow-patterns.md`\n\n- `.github/skills/agentic-workflow-designer/SKILL.md`\nAfter loading the matching workflow prompt or skill, follow it directly:\n- Design workflows from scratch via interview: `skills/agentic-workflow-designer/SKILL.md`\n- Create new workflows: `.github/aw/create-agentic-workflow.md`\n- Update existing workflows: `.github/aw/update-agentic-workflow.md`\n- Debug, audit, or investigate workflows: `.github/aw/debug-agentic-workflow.md`\n- Upgrade workflows and fix deprecations: `.github/aw/upgrade-agentic-workflows.md`\n- Create shared components or MCP wrappers: `.github/aw/create-shared-agentic-workflow.md`\n- Create report-generating workflows: `.github/aw/report.md`\n- Fix Dependabot manifest PRs: `.github/aw/dependabot.md`\n- Analyze coverage workflows: `.github/aw/test-coverage.md`\n- Render compact markdown charts: `.github/aw/asciicharts.md`\n- Map CLI commands to MCP usage: `.github/aw/cli-commands.md`\n- Choose workflow architecture and patterns: `.github/aw/patterns.md`\n- Optimize token usage and cost: `.github/aw/token-optimization.md`\n\nWhen 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 or skill.\n",".github/skills/benchmark/SKILL.md":"---\nname: benchmark\ndescription: Measure Z3 performance on a formula or file. Collects wall-clock time, theory solver statistics, memory usage, and conflict counts. Results are logged to z3agent.db for longitudinal tracking.\n---\n\nGiven an SMT-LIB2 formula or file, run Z3 with statistics enabled and report performance characteristics. This is useful for identifying performance regressions, comparing tactic strategies, and profiling theory solver workload distribution.\n\n# Step 1: Run Z3 with statistics\n\nAction:\n    Invoke benchmark.py with the formula or file. Use `--runs N` for\n    repeated timing.\n\nExpectation:\n    The script invokes `z3 -st`, parses the statistics block, and prints\n    a performance summary. A run entry is logged to z3agent.db.\n\nResult:\n    Timing and statistics are displayed. Proceed to Step 2 to interpret.\n\n```bash\npython3 scripts/benchmark.py --file problem.smt2\npython3 scripts/benchmark.py --file problem.smt2 --runs 5\npython3 scripts/benchmark.py --formula \"(declare-const x Int)...\" --debug\n```\n\n# Step 2: Interpret the output\n\nAction:\n    Review wall-clock time, memory usage, conflict counts, and per-theory\n    breakdowns.\n\nExpectation:\n    A complete performance profile including min/median/max timing when\n    multiple runs are requested.\n\nResult:\n    If performance is acceptable, no action needed.\n    If slow, try **simplify** to reduce the formula or adjust tactic strategies.\n\nThe output includes:\n\n- wall-clock time (ms)\n- result (sat/unsat/unknown/timeout)\n- memory usage (MB)\n- conflicts, decisions, propagations\n- per-theory breakdown (arithmetic, bv, array, etc.)\n\nWith `--runs N`, the script runs Z3 N times and reports min/median/max timing.\n\n# Step 3: Compare over time\n\nAction:\n    Query past benchmark runs from z3agent.db to detect regressions or\n    improvements.\n\nExpectation:\n    Historical run data is available for comparison, ordered by recency.\n\nResult:\n    If performance regressed, investigate recent formula or tactic changes.\n    If improved, record the successful configuration.\n\n```bash\npython3 ../../shared/z3db.py runs --skill benchmark --last 20\npython3 ../../shared/z3db.py query \"SELECT smtlib2, result, stats FROM formulas WHERE run_id IN (SELECT run_id FROM runs WHERE skill='benchmark') ORDER BY run_id DESC LIMIT 5\"\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula |\n| file | path | no | | path to .smt2 file |\n| runs | int | no | 1 | number of repeated runs for timing |\n| timeout | int | no | 60 | seconds per run |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/encode/SKILL.md":"---\nname: encode\ndescription: Translate constraint problems into SMT-LIB2 or Z3 Python API code. Handles common problem classes including scheduling, graph coloring, arithmetic puzzles, and verification conditions.\n---\n\nGiven a problem description (natural language, pseudocode, or a partial formulation), produce a complete, syntactically valid SMT-LIB2 encoding or Z3 Python script. The encoding should declare all variables, assert all constraints, and include the appropriate check-sat / get-model commands.\n\n# Step 1: Identify the problem class\n\nAction:\n    Determine the SMT theory and variable sorts required by the problem\n    description.\n\nExpectation:\n    A clear mapping from the problem to one of the supported theories\n    (LIA, LRA, QF_BV, etc.).\n\nResult:\n    If the theory is identified, proceed to Step 2. If the problem spans\n    multiple theories, select the appropriate combined logic.\n\n| Problem class | Theory | Typical sorts |\n|---------------|--------|---------------|\n| Integer arithmetic | LIA / NIA | Int |\n| Real arithmetic | LRA / NRA | Real |\n| Bitvector operations | QF_BV | (_ BitVec N) |\n| Arrays and maps | QF_AX | (Array Int Int) |\n| Strings and regex | QF_S | String, RegLan |\n| Uninterpreted functions | QF_UF | custom sorts |\n| Mixed theories | AUFLIA, etc. | combination |\n\n# Step 2: Generate the encoding\n\nAction:\n    Invoke encode.py with the problem description and desired output format.\n\nExpectation:\n    The script produces a complete SMT-LIB2 file or Z3 Python script with\n    all declarations, constraints, and check-sat commands.\n\nResult:\n    For `smtlib2` format: pass the output to **solve**.\n    For `python` format: execute the script directly.\n    Proceed to Step 3 for validation.\n\n```bash\npython3 scripts/encode.py --problem \"Find integers x, y such that x^2 + y^2 = 25 and x > 0\" --format smtlib2\npython3 scripts/encode.py --problem \"Schedule 4 tasks on 2 machines minimizing makespan\" --format python\n```\n\n# Step 3: Validate the encoding\n\nAction:\n    The script runs a syntax check by piping the output through `z3 -in`\n    in parse-only mode.\n\nExpectation:\n    No parse errors. If errors occur, the offending line is reported.\n\nResult:\n    On success: the encoding is ready for **solve**, **prove**, or **optimize**.\n    On parse error: fix the reported line and re-run.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| problem | string | yes | | problem description |\n| format | string | no | smtlib2 | output format: smtlib2 or python |\n| output | path | no | stdout | write to file instead of stdout |\n| validate | flag | no | on | run syntax check on the output |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/explain/SKILL.md":"---\nname: explain\ndescription: Parse and interpret Z3 output for human consumption. Handles models, unsat cores, proofs, statistics, and error messages. Translates solver internals into plain-language explanations.\n---\n\nGiven raw Z3 output (from the **solve**, **prove**, **optimize**, or **benchmark** skills), produce a structured explanation. This skill is for cases where the solver output is large, nested, or otherwise difficult to read directly.\n\n# Step 1: Identify the output type\n\nAction:\n    Determine the category of Z3 output to explain: model, core,\n    statistics, error, or proof.\n\nExpectation:\n    The output type maps to one of the recognized formats in the table below.\n\nResult:\n    If the type is ambiguous, use `--type auto` and let the script detect it.\n    Proceed to Step 2.\n\n| Output contains | Explanation type |\n|----------------|-----------------|\n| `(define-fun ...)` blocks | model explanation |\n| unsat core labels | conflict explanation |\n| `:key value` statistics | performance breakdown |\n| `(error ...)` | error diagnosis |\n| proof terms | proof sketch |\n\n# Step 2: Run the explainer\n\nAction:\n    Invoke explain.py with the output file or stdin.\n\nExpectation:\n    The script auto-detects the output type and produces a structured\n    plain-language summary.\n\nResult:\n    A formatted explanation is printed. If detection fails, re-run with\n    an explicit `--type` flag.\n\n```bash\npython3 scripts/explain.py --file output.txt\npython3 scripts/explain.py --stdin < output.txt\npython3 scripts/explain.py --file output.txt --debug\n```\n\n# Step 3: Interpret the explanation\n\nAction:\n    Review the structured explanation for accuracy and completeness.\n\nExpectation:\n    Models list each variable with its value and sort. Cores list\n    conflicting assertions. Statistics show time and memory breakdowns.\n\nResult:\n    Use the explanation to answer the user query or to guide the next\n    skill invocation.\n\nFor models:\n- Each variable is listed with its value and sort\n- Array and function interpretations are expanded\n- Bitvector values are shown in decimal and hex\n\nFor unsat cores:\n- The conflicting named assertions are listed\n- A minimal conflict set is highlighted\n\nFor statistics:\n- Time breakdown by phase (preprocessing, solving, model construction)\n- Theory solver load distribution\n- Memory high-water mark\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| file | path | no | | file containing Z3 output |\n| stdin | flag | no | off | read from stdin |\n| type | string | no | auto | force output type: model, core, stats, error |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/memory-safety/SKILL.md":"---\nname: memory-safety\ndescription: Run AddressSanitizer and UndefinedBehaviorSanitizer on the Z3 test suite to detect memory errors, undefined behavior, and leaks. Logs each finding to z3agent.db.\n---\n\nBuild Z3 with compiler-based sanitizer instrumentation, execute the test suite, and parse the runtime output for memory safety violations. Supported sanitizers are AddressSanitizer (heap and stack buffer overflows, use-after-free, double-free, memory leaks) and UndefinedBehaviorSanitizer (signed integer overflow, null pointer dereference, misaligned access, shift errors). Findings are deduplicated and stored in z3agent.db for triage and longitudinal tracking.\n\n# Step 1: Configure and build\n\nAction:\n    Invoke the script with the desired sanitizer flag. The script calls\n    cmake with the appropriate `-fsanitize` flags and builds the `test-z3`\n    target. Each sanitizer uses a separate build directory to avoid flag\n    conflicts.\n\nExpectation:\n    cmake configures successfully and make compiles the instrumented binary.\n    If a prior build exists with matching flags, only incremental compilation\n    runs.\n\nResult:\n    On success: an instrumented `test-z3` binary is ready in the build\n    directory. Proceed to Step 2.\n    On failure: verify compiler support for the requested sanitizer flags\n    and review cmake output.\n\n```bash\npython3 scripts/memory_safety.py --sanitizer asan\npython3 scripts/memory_safety.py --sanitizer ubsan\npython3 scripts/memory_safety.py --sanitizer both\n```\n\nTo reuse an existing build:\n```bash\npython3 scripts/memory_safety.py --sanitizer asan --skip-build --build-dir build/sanitizer-asan\n```\n\n# Step 2: Run and collect\n\nAction:\n    Execute the instrumented test binary with halt_on_error=0 so all\n    violations are reported rather than aborting on the first.\n\nExpectation:\n    The script parses AddressSanitizer, UndefinedBehaviorSanitizer, and\n    LeakSanitizer patterns from combined output, extracts source locations,\n    and deduplicates by category/file/line.\n\nResult:\n    On `clean`: no violations detected.\n    On `findings`: one or more violations found, each printed with severity,\n    category, message, and source location.\n    On `timeout`: test suite did not finish; increase timeout or investigate.\n    On `error`: build or execution failed before sanitizer output.\n\n```bash\npython3 scripts/memory_safety.py --sanitizer asan --timeout 900 --debug\n```\n\n# Step 3: Interpret results\n\nAction:\n    Review printed findings and query z3agent.db for historical comparison.\n\nExpectation:\n    Each finding includes severity, category, message, and source location.\n    The database query returns prior runs for trend analysis.\n\nResult:\n    On `clean`: no action required; proceed.\n    On `findings`: triage by severity and category. Compare against prior\n    runs to distinguish new regressions from known issues.\n    On `timeout`: increase the deadline or investigate a possible infinite\n    loop.\n    On `error`: inspect build logs before re-running.\n\nQuery past runs:\n```bash\npython3 ../../shared/z3db.py runs --skill memory-safety --last 10\npython3 ../../shared/z3db.py query \"SELECT category, severity, file, line, message FROM findings WHERE run_id IN (SELECT run_id FROM runs WHERE skill='memory-safety') ORDER BY run_id DESC LIMIT 20\"\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| sanitizer | choice | no | asan | which sanitizer to enable: asan, ubsan, or both |\n| build-dir | path | no | build/sanitizer-{name} | path to the build directory |\n| timeout | int | no | 600 | seconds before killing the test run |\n| skip-build | flag | no | off | reuse an existing instrumented build |\n| debug | flag | no | off | verbose cmake, make, and test output |\n| db | path | no | .z3-agent/z3agent.db | path to the logging database |\n",".github/skills/optimize/SKILL.md":"---\nname: optimize\ndescription: Solve constrained optimization problems using Z3. Supports minimization and maximization of objective functions over integer, real, and bitvector domains.\n---\n\nGiven a set of constraints and an objective function, find the optimal value. Z3 supports both hard constraints (must hold) and soft constraints (weighted preferences), as well as lexicographic multi-objective optimization.\n\n# Step 1: Formulate the problem\n\nAction:\n    Write constraints and an objective using `(minimize ...)` or\n    `(maximize ...)` directives, followed by `(check-sat)` and `(get-model)`.\n\nExpectation:\n    A valid SMT-LIB2 formula with at least one optimization directive and\n    all variables declared.\n\nResult:\n    If the formula is well-formed, proceed to Step 2. For multi-objective\n    problems, list directives in priority order for lexicographic optimization.\n\nExample: minimize `x + y` subject to `x >= 1`, `y >= 2`, `x + y <= 10`:\n```smtlib\n(declare-const x Int)\n(declare-const y Int)\n(assert (>= x 1))\n(assert (>= y 2))\n(assert (<= (+ x y) 10))\n(minimize (+ x y))\n(check-sat)\n(get-model)\n```\n\n# Step 2: Run the optimizer\n\nAction:\n    Invoke optimize.py with the formula or file path.\n\nExpectation:\n    The script prints `sat` with the optimal assignment, `unsat`, `unknown`,\n    or `timeout`. A run entry is logged to z3agent.db.\n\nResult:\n    On `sat`: proceed to Step 3 to read the optimal values.\n    On `unsat` or `timeout`: check constraints for contradictions or simplify.\n\n```bash\npython3 scripts/optimize.py --file scheduling.smt2\npython3 scripts/optimize.py --formula \"<inline smt-lib2>\" --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Parse the objective value and satisfying assignment from the output.\n\nExpectation:\n    `sat` with a model containing the optimal value, `unsat` indicating\n    infeasibility, or `unknown`/`timeout`.\n\nResult:\n    On `sat`: report the optimal value and assignment.\n    On `unsat`: the constraints are contradictory, no feasible solution exists.\n    On `unknown`/`timeout`: relax constraints or try **simplify**.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula with minimize/maximize |\n| file | path | no | | path to .smt2 file |\n| timeout | int | no | 60 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/prove/SKILL.md":"---\nname: prove\ndescription: Prove validity of logical statements by negation and satisfiability checking. If the negation is unsatisfiable, the original statement is valid. Otherwise a counterexample is returned.\n---\n\nGiven a conjecture (an SMT-LIB2 assertion or a natural language claim), determine whether it holds universally. The method is standard: negate the conjecture and check satisfiability. If the negation is unsatisfiable, the original is valid. If satisfiable, the model is a counterexample.\n\n# Step 1: Prepare the negated formula\n\nAction:\n    Wrap the conjecture in `(assert (not ...))` and append\n    `(check-sat)(get-model)`.\n\nExpectation:\n    A complete SMT-LIB2 formula that negates the original conjecture with\n    all variables declared.\n\nResult:\n    If the negation is well-formed, proceed to Step 2.\n    If the conjecture is natural language, run **encode** first.\n\nExample: to prove that `(> x 3)` implies `(> x 1)`:\n```smtlib\n(declare-const x Int)\n(assert (not (=> (> x 3) (> x 1))))\n(check-sat)\n(get-model)\n```\n\n# Step 2: Run the prover\n\nAction:\n    Invoke prove.py with the conjecture and variable declarations.\n\nExpectation:\n    The script prints `valid`, `invalid` (with counterexample), `unknown`,\n    or `timeout`. A run entry is logged to z3agent.db.\n\nResult:\n    On `valid`: proceed to **explain** if the user needs a summary.\n    On `invalid`: report the counterexample directly.\n    On `unknown`/`timeout`: try **simplify** first, or increase the timeout.\n\n```bash\npython3 scripts/prove.py --conjecture \"(=> (> x 3) (> x 1))\" --vars \"x:Int\"\n```\n\nFor file input where the file contains the full negated formula:\n```bash\npython3 scripts/prove.py --file negated.smt2\n```\n\nWith debug tracing:\n```bash\npython3 scripts/prove.py --conjecture \"(=> (> x 3) (> x 1))\" --vars \"x:Int\" --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Read the prover output to determine validity of the conjecture.\n\nExpectation:\n    One of `valid`, `invalid` (with counterexample), `unknown`, or `timeout`.\n\nResult:\n    On `valid`: the conjecture holds universally.\n    On `invalid`: the model shows a concrete counterexample.\n    On `unknown`/`timeout`: the conjecture may require auxiliary lemmas or induction.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| conjecture | string | no | | the assertion to prove (without negation) |\n| vars | string | no | | variable declarations as \"name:sort\" pairs, comma-separated |\n| file | path | no | | .smt2 file with the negated formula |\n| timeout | int | no | 30 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\nEither `conjecture` (with `vars`) or `file` must be provided.\n",".github/skills/simplify/SKILL.md":"---\nname: simplify\ndescription: Reduce formula complexity using Z3 tactic chains. Supports configurable tactic pipelines for boolean, arithmetic, and bitvector simplification.\n---\n\nGiven a formula, apply a sequence of Z3 tactics to produce an equivalent but simpler form. This is useful for understanding what Z3 sees after preprocessing, debugging tactic selection, and reducing formula size before solving.\n\n# Step 1: Choose tactics\n\nAction:\n    Select a tactic chain from the available Z3 tactics based on the\n    formula's theory.\n\nExpectation:\n    A comma-separated list of tactic names suitable for the formula domain.\n\nResult:\n    If unsure, use the default chain: `simplify,propagate-values,ctx-simplify`.\n    For bitvector formulas, add `bit-blast`. Proceed to Step 2.\n\n| Tactic | What it does |\n|--------|-------------|\n| simplify | constant folding, algebraic identities |\n| propagate-values | substitute known equalities |\n| ctx-simplify | context-dependent simplification |\n| elim-uncnstr | remove unconstrained variables |\n| solve-eqs | Gaussian elimination |\n| bit-blast | reduce bitvectors to booleans |\n| tseitin-cnf | convert to CNF |\n| aig | and-inverter graph reduction |\n\n# Step 2: Run simplification\n\nAction:\n    Invoke simplify.py with the formula and optional tactic chain.\n\nExpectation:\n    The script applies each tactic in sequence and prints the simplified\n    formula. A run entry is logged to z3agent.db.\n\nResult:\n    If the output is simpler, pass it to **solve** or **prove**.\n    If unchanged, try a different tactic chain.\n\n```bash\npython3 scripts/simplify.py --formula \"(assert (and (> x 0) (> x 0)))\" --vars \"x:Int\"\npython3 scripts/simplify.py --file formula.smt2 --tactics \"simplify,propagate-values,ctx-simplify\"\npython3 scripts/simplify.py --file formula.smt2 --debug\n```\n\nWithout `--tactics`, the script applies the default chain: `simplify`, `propagate-values`, `ctx-simplify`.\n\n# Step 3: Interpret the output\n\nAction:\n    Read the simplified formula output in SMT-LIB2 syntax.\n\nExpectation:\n    One or more `(assert ...)` blocks representing equivalent subgoals.\n\nResult:\n    A smaller formula indicates successful reduction. Pass the result to\n    **solve**, **prove**, or **optimize** as needed.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula to simplify |\n| vars | string | no | | variable declarations as \"name:sort\" pairs |\n| file | path | no | | path to .smt2 file |\n| tactics | string | no | simplify,propagate-values,ctx-simplify | comma-separated tactic names |\n| timeout | int | no | 30 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n",".github/skills/solve/SKILL.md":"---\nname: solve\ndescription: Check satisfiability of SMT-LIB2 formulas using Z3. Returns sat/unsat with models or unsat cores. Logs every invocation to z3agent.db for auditability.\n---\n\nGiven an SMT-LIB2 formula (or a set of constraints described in natural language), determine whether the formula is satisfiable. If sat, extract a satisfying assignment. If unsat and tracking labels are present, extract the unsat core.\n\n# Step 1: Prepare the formula\n\nAction:\n    Convert the input to valid SMT-LIB2. If the input is natural language,\n    use the **encode** skill first.\n\nExpectation:\n    A syntactically valid SMT-LIB2 formula ending with `(check-sat)` and\n    either `(get-model)` or `(get-unsat-core)` as appropriate.\n\nResult:\n    If valid SMT-LIB2 is ready, proceed to Step 2.\n    If encoding is needed, run **encode** first and return here.\n\n# Step 2: Run Z3\n\nAction:\n    Invoke solve.py with the formula string or file path.\n\nExpectation:\n    The script pipes the formula to `z3 -in`, logs the run to\n    `.z3-agent/z3agent.db`, and prints the result.\n\nResult:\n    Output is one of `sat`, `unsat`, `unknown`, or `timeout`.\n    Proceed to Step 3 to interpret.\n\n```bash\npython3 scripts/solve.py --formula \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\"\n```\n\nFor file input:\n```bash\npython3 scripts/solve.py --file problem.smt2\n```\n\nWith debug tracing:\n```bash\npython3 scripts/solve.py --file problem.smt2 --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Parse the Z3 output to determine satisfiability and extract any model\n    or unsat core.\n\nExpectation:\n    `sat` with a model, `unsat` optionally with a core, `unknown`, or\n    `timeout`.\n\nResult:\n    On `sat`: report the model to the user.\n    On `unsat`: report the core if available.\n    On `unknown`/`timeout`: try **simplify** or increase the timeout.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula as a string |\n| file | path | no | | path to an .smt2 file |\n| timeout | int | no | 30 | seconds before killing z3 |\n| z3 | path | no | auto | explicit path to z3 binary |\n| debug | flag | no | off | print z3 command, stdin, stdout, stderr, timing |\n| db | path | no | .z3-agent/z3agent.db | path to the logging database |\n\nEither `formula` or `file` must be provided.\n",".github/skills/static-analysis/SKILL.md":"---\nname: static-analysis\ndescription: Run Clang Static Analyzer (scan-build) on Z3 source and log structured findings to z3agent.db.\n---\n\nRun the Clang Static Analyzer over a CMake build of Z3, parse the resulting plist diagnostics, and record each finding with file, line, category, and description. This skill wraps scan-build into a reproducible, logged workflow suitable for regular analysis sweeps and regression tracking.\n\n# Step 1: Run the analysis\n\nAction:\n    Invoke the script pointing at the CMake build directory. The script\n    runs `scan-build cmake -S . -B <build-dir>` followed by a scan-build-wrapped\n    `cmake --build` and writes\n    checker output to the output directory.\n\nExpectation:\n    scan-build completes within the timeout, producing plist diagnostic\n    files in the output directory (defaults to a `scan-results` subdirectory\n    of the build directory).\n\nResult:\n    On success: diagnostics are parsed and findings are printed. Proceed to\n    Step 2.\n    On failure: verify that clang and scan-build are installed and that the\n    build directory contains a valid CMake configuration.\n\n```bash\npython3 scripts/static_analysis.py --build-dir build\npython3 scripts/static_analysis.py --build-dir build --output-dir /tmp/sa-results --debug\npython3 scripts/static_analysis.py --build-dir build --timeout 1800\n```\n\n# Step 2: Interpret the output\n\nAction:\n    Review the printed findings and the summary table grouped by category.\n\nExpectation:\n    Each finding shows its source location, category, and description.\n    The summary table ranks categories by frequency for quick triage.\n\nResult:\n    On zero findings: the codebase passes all enabled static checks.\n    On findings: prioritize by category frequency and severity. Address\n    null dereferences and use-after-free classes first.\n\nExample output:\n\n```\n[Dead store] src/ast/ast.cpp:142: Value stored to 'result' is never read\n[Null dereference] src/smt/theory_lra.cpp:87: Access to field 'next' results in a dereference of a null pointer\n```\n\n# Step 3: Review historical findings\n\nAction:\n    Query z3agent.db to compare current results against prior analysis\n    runs.\n\nExpectation:\n    Queries return category counts and run history, enabling regression\n    detection across commits.\n\nResult:\n    On stable or decreasing counts: no regressions introduced.\n    On increased counts: cross-reference new findings with recent commits\n    to identify the responsible change.\n\n```bash\npython3 ../../shared/z3db.py query \"SELECT category, COUNT(*) as cnt FROM findings WHERE run_id IN (SELECT run_id FROM runs WHERE skill='static-analysis') GROUP BY category ORDER BY cnt DESC\"\npython3 ../../shared/z3db.py runs --skill static-analysis --last 10\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| build-dir | path | yes | | path to the CMake build directory |\n| output-dir | path | no | BUILD/scan-results | directory for scan-build output |\n| timeout | int | no | 1200 | seconds allowed for the full build |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n| debug | flag | no | off | verbose tracing |\n"},"items":[{"name":"copilot-instructions.md","path":".github/copilot-instructions.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/copilot-instructions.md","title":"GitHub Copilot Instructions","category":"copilot-instructions","format":"markdown","content":"# Z3 Theorem Prover Development Guide\n\nAlways reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here.\n\n## Working Effectively\n\n### Bootstrap and Build the Repository\n\nZ3 is built with CMake:\n- `cmake -S . -B build` -- takes 1 second to configure\n- `cmake --build build --parallel $(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Dependencies and Requirements\n- Python 3.x (required to run CMake's code generation scripts)\n- C++20 capable compiler (g++ or clang++)\n- Git (for version information)\n\n### Test the Repository\n\n- Build unit tests: `cmake --build build --target test-z3 --parallel $(nproc)` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**Test basic Z3 functionality:**\n```bash\n./z3 --version\necho \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\" | ./z3 -in\n```\n\n### Validation Scenarios\n\n**ALWAYS** test these scenarios after making changes:\n\n#### Basic SMT Solving\n```bash\ncd build\necho \"(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(get-model)\" | ./z3 -in\n```\nExpected output: `sat` followed by a model showing `x = 1` or similar.\n\n#### Python Bindings\n```bash\ncd build/python\npython3 -c \"import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())\"\n```\nExpected output: `Result: sat` and `Model: [x = 1]` or similar.\n\n#### Command Line Help\n```bash\n./z3 --help | head -10\n```\nShould display version and usage information.\n\n## Build System Details\n\n### CMake Build System\n- Configuration: `cmake -S . -B build` (1 second)\n- Main build: `cmake --build build --parallel $(nproc)` (17 minutes)\n- Creates Python bindings in `build/python/` when `-DZ3_BUILD_PYTHON_BINDINGS=ON` is set\n- Out-of-source build: clean build tree, no source pollution\n\n### Critical Timing and Timeout Requirements\n\n**NEVER CANCEL these operations**:\n- `cmake --build build --parallel $(nproc)`: 15-17 minutes. **Set timeout to 30+ minutes minimum**.\n- `cmake --build build --target test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**.\n- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**.\n\n**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing.\n\n## Repository Structure\n\n### Key Directories\n- `src/` - Main source code organized by components (ast, smt, sat, etc.)\n- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.)\n- `scripts/` - Build scripts and utilities\n- `.github/workflows/` - CI/CD pipeline definitions\n- `cmake/` - CMake configuration files\n\n### Important Files\n- `README.md` - Main documentation and build instructions\n- `README-CMake.md` - Detailed CMake build documentation\n- `CMakeLists.txt` - Main CMake configuration\n\n## Common Tasks and Validation\n\n### Pre-commit Validation\nBefore committing changes:\n1. **Build successfully**: Use one of the validated build commands above\n2. **Run unit tests**: `./test-z3 /a` must pass\n3. **Test basic functionality**: Run validation scenarios above\n4. **Test affected language bindings**: If modifying API, test relevant examples\n\n### Working with Language Bindings\n- **Python**: Located in `build/python/`, test with validation scenario above\n- **C/C++**: Examples in `examples/c/` and `examples/c++/`\n  - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example`\n  - Run with: `LD_LIBRARY_PATH=build ./test_example`\n- **Java**: Build with `cmake -S . -B build -DZ3_BUILD_JAVA_BINDINGS=ON`, examples in `examples/java/`\n- **C#/.NET**: Build with `cmake -S . -B build -DZ3_BUILD_DOTNET_BINDINGS=ON`, examples in `examples/dotnet/`\n\n### Performance Testing\nFor performance-sensitive changes:\n- Build optimized: `cmake -S . -B build -DCMAKE_BUILD_TYPE=Release` (Release mode)\n- Test with realistic SMT problems from `examples/SMT-LIB2/`\n- Use Z3's built-in statistics: `z3 -st problem.smt2`\n\n## Common Issues and Solutions\n\n### Python Import Errors\n- **Error**: `import z3` fails\n- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH`\n\n### Missing Dependencies\n- **Error**: Compiler not found or version too old\n- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+\n\n### Long Build Times\n- **Normal**: 15-17 minute builds are expected for Z3\n- **Never cancel**: Set timeouts appropriately and wait for completion\n- **Optimization**: Use `cmake --build build --parallel $(nproc)` for parallel compilation\n\n## Key Projects in Codebase\n\nZ3 is organized into several key components:\n\n- **Core SMT**: `src/smt/` - Main SMT solver engine\n- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver  \n- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.)\n- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation\n- **Tactics**: `src/tactic/` - Configurable solving strategies\n- **API**: `src/api/` - Public C API and language bindings\n- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers\n- **Model Generation**: Creating and manipulating satisfying assignments\n\nThe architecture is modular with clean separation between the core solver, theory plugins, and user interfaces.\n","isInternal":false,"tokens":1452,"sizeBytes":5477},{"name":"SKILL.md","path":".github/skills/agentic-workflow-designer/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/agentic-workflow-designer/SKILL.md","title":"agentic-workflow-designer","category":"anthropic-skill","format":"markdown","content":"---\nname: agentic-workflow-designer\ndescription: Conversational skill that interviews users to design new agentic workflows\ndisable-model-invocation: true\n---\n\n# Workflow Designer\n\nUse this skill to run a structured interview with users who know their goal but not the workflow syntax yet, then generate one complete workflow `.md` file.\n\n## When to Use This Skill\n\nUse this before `.github/aw/create-agentic-workflow.md` when requirements are unclear or incomplete.\n\n- Use `skills/agentic-workflow-designer/SKILL.md` to discover and confirm requirements.\n- Use `.github/aw/create-agentic-workflow.md` once requirements are clear and ready for implementation.\n- Use `.github/aw/agentic-chat.md` when the user wants a specification/pseudo-code instead of a runnable workflow file.\n\n## Interview Framework\n\nAsk one question at a time. Move to the next phase only after the current phase is clear.\n\n### Phase 1: Goal\n\nAsk: **\"What do you want to automate?\"**\n\nCapture:\n- Workflow name (kebab-case candidate)\n- Brief description\n- Optional emoji\n\n### Phase 2: Trigger\n\nAsk: **\"When should this run?\"**\n\nFollow up only if needed:\n- Which event type(s)?\n- Any filters (labels, branches, commands)?\n- Scheduled cadence (daily/weekly/hourly)?\n\nMap to the `on:` block.\n\n### Phase 3: Scope (Read/Write)\n\nAsk:\n- **\"What should it read?\"** (issues, PRs, code, discussions, CI data)\n- **\"What should it create or update?\"** (comments, issues, PRs, labels)\n\nMap to:\n- `permissions:` (keep read-only for agent job)\n- `tools:`\n- `safe-outputs:`\n\n### Phase 4: Data Strategy\n\nAsk:\n- **\"What data does the agent need to make decisions?\"**\n- Follow up: **\"Can we pre-fetch and aggregate that data with shell commands so the agent only reads compact JSON?\"**\n\nCapture:\n- Whether `steps:` should pre-fetch GitHub data with `gh` + `jq`\n- Output paths under `/tmp/gh-aw/data/`\n- Whether batch work should use sub-agents\n\nMap to:\n- `steps:`\n- Prompt references to pre-computed file paths\n\n### Phase 5: Guardrails\n\nAsk: **\"Should it block merging, just advise, or silently log?\"**\n\nCapture:\n- Visibility expectations (comment, issue, no visible output)\n- No-op behavior expectation\n\nGuide toward safe output behavior and explicit `noop` instructions.\n\n### Phase 6: Context & Network\n\nAsk: **\"Does it need external APIs, web access, package installs, or MCP servers?\"**\n\nFollow up:\n- **\"Any third-party services or MCP servers to include (for example Slack, Jira, Datadog, custom internal MCP)?\"**\n- **\"Are you deploying on GitHub.com, GHEC with custom endpoints, or GHES?\"**\n- For each integration, identify required auth from source docs and map it to GitHub Actions secrets + workflow env variables.\n- Ask for exact external domains (FQDN/wildcard).\n\nMap to:\n- `network.allowed`\n- Optional MCP/GitHub tool usage in `tools:`\n- `secrets:` / `env:` wiring for integration tokens\n- GHES/GHEC settings such as `engine.api-target` and `aw.json` `ghes: true` (when applicable)\n\n### Phase 7: Engine (optional)\n\nAsk only if ambiguous: **\"Any AI engine preference?\"**\n\nIf no preference, suggest default:\n- \"I'd suggest Copilot since you haven't mentioned a preference. Sound good?\"\n\nMap to `engine:` only when not default.\n\n### Phase 8: Confirmation\n\nPresent a structured summary and ask for approval before generation.\n\n## Decision Heuristics\n\n### Trigger Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"when someone opens a PR\" | `on: pull_request:` with `types: [opened]` |\n| \"when a PR is updated\" | `on: pull_request:` with `types: [opened, synchronize]` |\n| \"every morning\", \"daily\" | fuzzy schedule shorthand `on: schedule: daily on weekdays` (compiler expands to cron) |\n| \"every Monday\", \"weekly\" | fuzzy schedule shorthand `on: schedule: weekly` (compiler expands to cron) |\n| \"when I say /review\" | `on: slash_command:` with `name: review` (or requested command) |\n| \"when an issue is labeled bug\" | `on: issues:` with `types: [labeled]` and label filter guidance |\n| \"run when label ai-review is added\" | `on: label_command:` with `name`/`names`, optional event scoping, and label-as-command semantics |\n| \"run on PRs from forks\" | `on: pull_request:` plus explicit `forks:` allowlist and fork security guardrails |\n| \"sometimes automatic, sometimes manual\" | semi-active pattern: combine `schedule`/event triggers with `workflow_dispatch` |\n| \"manually\", \"on demand\" | `on: workflow_dispatch:` |\n| \"when a deployment fails\" | `on: deployment_status:` |\n| \"when another workflow finishes\" | `on: workflow_run:` |\n\n### Safe Output Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"post a comment\" | `add-comment` |\n| \"create an issue\" | `create-issue` |\n| \"update issue title/body\" | `update-issue` |\n| \"close the issue\" | `close-issue` |\n| \"assign someone\", \"remove assignment\" | `assign-to-user`, `unassign-from-user` |\n| \"set issue type/field/milestone\" | `set-issue-type`, `set-issue-field`, `assign-milestone` |\n| \"open a PR\", \"submit changes\" | `create-pull-request` |\n| \"update PR description/title\" | `update-pull-request` |\n| \"close the PR\", \"merge the PR\" | `close-pull-request`, `merge-pull-request` |\n| \"mark PR ready\", \"sync PR branch\" | `mark-pull-request-as-ready-for-review`, `update-branch` |\n| \"commit a fix to the PR branch\" | `push-to-pull-request-branch` |\n| \"approve / request changes\" | `submit-pull-request-review` |\n| \"inline review comment\", \"reply to review thread\" | `create-pull-request-review-comment`, `reply-to-pull-request-review-comment`, `resolve-pull-request-review-thread` |\n| \"start or edit discussion\", \"close discussion\" | `create-discussion`, `update-discussion`, `close-discussion` |\n| \"request reviewer\", \"hide comment\" | `add-reviewer`, `hide-comment` |\n| \"create/update project\", \"project status update\" | `create-project`, `update-project`, `create-project-status-update` |\n| \"update release\", \"upload release asset\" | `update-release`, `upload-asset` |\n| \"create/auto-fix code scan alert\" | `create-code-scanning-alert`, `autofix-code-scanning-alert` |\n| \"start an agent session\", \"assign to an agent\" | `create-agent-session`, `assign-to-agent` |\n| \"store persistent memory comment\" | `comment-memory` |\n| \"link a sub-issue\" | `link-sub-issue` |\n| \"add labels\", \"remove labels\" | `add-labels`, `remove-labels` |\n| \"nothing visible\", \"just analyze\" | no safe outputs required |\n\n### Network Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"calls an external API\" | ask for exact FQDN/wildcard, then add to `network.allowed` |\n| \"reads GitHub data / clones repos\" | include `github` in `network.allowed` |\n| \"uses GitHub Actions artifacts or cache\" | include `github-actions` in `network.allowed` |\n| \"installs npm packages\" | include `node` in `network.allowed` |\n| \"runs pip install\" | include `python` in `network.allowed` |\n| \"builds Go code\" | include `go` in `network.allowed` |\n| \"installs gems / uses Bundler\" | include `ruby` in `network.allowed` |\n| \"runs cargo build\" | include `rust` in `network.allowed` |\n| \"uses NuGet / .NET restore\" | include `dotnet` in `network.allowed` |\n| \"builds with Maven / Gradle\" | include `java` in `network.allowed` |\n| \"uses Docker / pulls container images / pushes to GHCR\" | include `containers` in `network.allowed` |\n| \"runs Playwright browser tests\" | include `playwright` in `network.allowed` |\n| \"runs apt install / yum / apk\" | include `linux-distros` in `network.allowed` |\n| \"uses Terraform / HashiCorp registry\" | include `terraform` in `network.allowed` |\n| \"connects to localhost / loopback / local services\" | include `local` in `network.allowed` |\n| \"uses Swift Package Manager\" | include `swift` in `network.allowed` |\n| \"uses Composer / PHP packages\" | include `php` in `network.allowed` |\n| \"uses pub.dev / Dart packages\" | include `dart` in `network.allowed` |\n| \"uses Hackage / Haskell packages\" | include `haskell` in `network.allowed` |\n| \"uses CPAN / Perl packages\" | include `perl` in `network.allowed` |\n| \"serves or loads web fonts\" | include `fonts` in `network.allowed` |\n| \"uses Deno or JSR packages\" | include `deno` in `network.allowed` |\n| \"uses Elixir / Hex packages\" | include `elixir` in `network.allowed` |\n| \"uses Bazel build\" | include `bazel` in `network.allowed` |\n| \"uses R / CRAN packages\" | include `r` in `network.allowed` |\n| \"no external access\" | `network.allowed: [defaults]` (or `[]` if explicitly zero network) |\n\n### Tool Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"read GitHub issues/PRs/workflows\" | `tools.github` with `mode: gh-proxy` and minimal `toolsets` |\n| \"use full MCP server/tool definitions\" | `tools.github` with `mode: local` |\n| \"use other MCP servers but keep token cost down\" | `tools.cli-proxy: true` (hybrid CLI-proxy mode) |\n| \"edit files\" | `edit` tool (default unless restricted) |\n| \"run commands/tests\" | `bash` tool (default unless restricted) |\n| \"browse web pages/docs\" | `web-fetch` and/or `web-search` |\n| \"test UI flows\" | `playwright` |\n\n### Pattern Heuristics\n\n| User says... | Recommended named pattern |\n|---|---|\n| \"triage issues automatically\" | `IssueOps` |\n| \"run on /commands with human approval loops\" | `ChatOps` |\n| \"run every weekday and keep improving\" | `DailyOps` |\n| \"monitor workflow failures and trends\" | `MonitorOps` |\n| \"process a big backlog in chunks\" | `BatchOps` |\n| \"run manually with input parameters\" | `DispatchOps` |\n| \"apply a label-based workflow\" | `LabelOps` |\n| \"operate across multiple repositories\" | `MultiRepoOps` |\n| \"coordinate multiple sub-agents\" | `Orchestration` |\n| \"manage project board items\" | `ProjectOps` |\n| \"research, plan, and assign issues\" | `ResearchPlanAssignOps` |\n| \"self-correcting / retry on failure\" | `CorrectionOps` |\n| \"run in a side/fork repo\" | `SideRepoOps` |\n| \"write a spec before implementing\" | `SpecOps` |\n| \"A/B test workflow variants\" | `TrialOps` |\n| \"process items from a queue\" | `WorkQueueOps` |\n| \"deterministic, no LLM needed\" | `DeterministicOps` |\n| \"manage from a central repo\" | `CentralRepoOps` |\n| \"track work via GitHub Projects\" | `Monitoring with Projects` |\n\n### Integration Auth Mapping\n\nWhen the user names a third-party service or MCP server:\n\n1. Confirm whether native tool, MCP server, or safe-output job is the right integration path.\n2. Look up the integration's auth requirements and required scopes before finalizing the design.\n3. Provide a concrete setup checklist with:\n   - required GitHub Actions secrets (names to create)\n   - workflow env variables that consume those secrets\n   - minimum token scopes/permissions needed\n\nOutput format to use:\n\n```text\nIntegration auth setup:\n- <service-or-mcp>: <purpose>\n  - Secrets to create: <SECRET_NAME>, <SECRET_NAME>\n  - Workflow env vars: <ENV_VAR>=${{ secrets.<SECRET_NAME> }}\n  - Required scopes/permissions: <least-privilege scopes>\n```\n\nNever suggest committing plaintext tokens.\n\n### Data Strategy Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"analyze PRs\", \"review issues\", \"check status\" | add `steps:` that pre-fetch with `gh` + `jq` |\n| \"read the diff\", \"look at changed files\" | add `steps:` using `gh pr diff` or `gh pr view --json files` |\n| \"search for patterns across repos\" | add `steps:` using `gh search` + `jq` filters |\n| \"just respond to a comment\" | no pre-fetch needed (event payload is enough) |\n| \"process each item individually\" | suggest sub-agent pattern with `model: small` |\n\n## Token Optimization Defaults\n\nApply these defaults unless the user explicitly asks otherwise:\n\n1. Use DataOps by default for GitHub reads: pre-fetch/aggregate with `gh` + `jq` in `steps:`, store compact JSON in `/tmp/gh-aw/data/`, and point the prompt to those files (see `.github/aw/token-optimization.md` for details).\n2. Keep tool surface minimal: default to `tools.github.mode: gh-proxy`, include only required toolsets, and prefer `bash` + `gh` for simple reads.\n3. For batch workloads, split items into compact data and suggest sub-agent processing with `model: small`.\n4. Keep prompts compact: concise imperative instructions, explicit file paths, single-line `noop` guidance, and stable instructions before dynamic content.\n\n## Progressive Disclosure Rules\n\n1. Never dump all options at once; ask one targeted question at a time.\n2. Skip questions when answers are inferable from prior user statements.\n3. Offer smart defaults and request confirmation instead of over-questioning.\n4. Ask at most 5 questions before presenting a summary; then ask \"anything else?\" if needed.\n5. Detect done signals (`that's it`, `looks good`, `generate it`) and proceed to generation.\n\n## Confirmation Format\n\nUse this exact structure:\n\n```text\n📋 Proposed workflow:\n- Name: <workflow-id>\n- Trigger: <event + key options>\n- Engine: <engine or default>\n- Tools: <tool summary>\n- Safe outputs: <list or none>\n- Network: <allowed summary>\n- Integrations/Auth: <service/mcp + required secrets/env vars>\n- Deployment: <GitHub.com or GHEC/GHES details>\n- Intent: <one-sentence task>\n```\n\nThen ask: **\"Ready to generate, or want to adjust anything?\"**\n\n## Generation Template\n\nAfter confirmation, generate one workflow file using the same skeleton style as `.github/aw/create-agentic-workflow.md`.\n\n```markdown\n---\nemoji: <emoji>\ndescription: <brief description>\non:\n  <trigger config>\npermissions:\n  contents: read\n  issues: read\n  pull-requests: read\ntools:\n  github:\n    mode: gh-proxy\n    toolsets: [default]\nsteps:\n  - name: <optional data prefetch>\n    run: |\n      mkdir -p /tmp/gh-aw/data\n      <gh + jq commands that produce compact JSON>\nsafe-outputs:\n  <safe-output-types-if-needed>\nnetwork:\n  allowed:\n    - defaults\n    - <additional entries if needed>\n---\n\n# <Workflow Name>\n\n## Task\n\n<clear instructions tied to trigger context>\nIf `steps:` includes pre-fetch commands, read the resulting `/tmp/gh-aw/data/*.json` files instead of broad live re-fetches.\n\n## Safe Outputs\n\n- Use configured safe outputs for all visible write actions.\n- Call `noop` with a short reason when no action is needed.\n```\n\n## Validation Checklist\n\nBefore final output, run this internal self-check:\n\n- [ ] Agent job permissions remain read-only (writes only via safe outputs)\n- [ ] `safe-outputs:` covers every write action mentioned in prompt/instructions\n- [ ] Network access is scoped; avoid blanket wildcard entries\n- [ ] Trigger matches the user's intended activation event\n- [ ] Prompt instructs agent to call `noop` when no action is needed\n- [ ] Unnecessary defaults are omitted (for example `engine: copilot`)\n- [ ] If reading GitHub data, `steps:` pre-fetches compact JSON (DataOps)\n- [ ] `tools.github.mode` is `gh-proxy` unless broader MCP toolsets are explicitly needed\n- [ ] Only required toolsets are listed (avoid blanket toolset lists)\n- [ ] Prompt references specific pre-computed file paths\n- [ ] For batch processing (>5 items), sub-agent pattern is suggested\n- [ ] For each third-party service/MCP integration, required secrets/env vars are listed\n- [ ] Auth guidance includes least-privilege token scope recommendations\n- [ ] For GHEC/GHES deployments, `engine.api-target` and GHES compatibility guidance are included when needed\n\n## References (load only when needed)\n\nIn-repo references:\n- `.github/aw/syntax.md` (index → `.github/aw/syntax-core.md`, `.github/aw/syntax-agentic.md`, `.github/aw/syntax-tools-imports.md`)\n- `.github/aw/safe-outputs.md` (index → `.github/aw/safe-outputs-content.md`, `.github/aw/safe-outputs-management.md`, `.github/aw/safe-outputs-automation.md`, `.github/aw/safe-outputs-runtime.md`)\n- `.github/aw/network.md`\n- `.github/aw/patterns.md`\n- `.github/aw/subagents.md`\n- `.github/aw/token-optimization.md`\n- `.github/aw/triggers.md`\n- `.github/aw/create-agentic-workflow.md`\n\nPortable HTTPS references:\n- `https://github.com/github/gh-aw/blob/main/.github/aw/syntax.md` (index → `.../syntax-core.md`, `.../syntax-agentic.md`, `.../syntax-tools-imports.md`)\n- `https://github.com/github/gh-aw/blob/main/.github/aw/safe-outputs.md` (index → `.../safe-outputs-content.md`, `.../safe-outputs-management.md`, `.../safe-outputs-automation.md`, `.../safe-outputs-runtime.md`)\n- `https://github.com/github/gh-aw/blob/main/.github/aw/network.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/patterns.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/triggers.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/create-agentic-workflow.md`\n","frontmatter":{"name":"agentic-workflow-designer","description":"Conversational skill that interviews users to design new agentic workflows","disable-model-invocation":true,"disableModelInvocation":true},"isInternal":false,"tokens":4195,"sizeBytes":16314},{"name":"SKILL.md","path":".github/skills/agentic-workflows/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/agentic-workflows/SKILL.md","title":"agentic-workflows","category":"anthropic-skill","format":"markdown","content":"---\nname: agentic-workflows\ndescription: Route gh-aw workflow design/create/debug/upgrade requests to the right prompts.\n---\n\n# Agentic Workflows Router\n\nUse this skill when a user asks to design, create, update, debug, or upgrade GitHub Agentic Workflows in this repository.\n\nThis skill is a dispatcher: identify the task type, load the matching workflow prompt/skill file, and follow it directly. Keep responses concise and ask a clarifying question if the correct prompt is unclear.\n\nRead only the files you need:\nLoad these files from `github/gh-aw` (they are not available locally).\n- `.github/aw/agentic-chat.md`\n- `.github/aw/agentic-workflows-mcp.md`\n- `.github/aw/asciicharts.md`\n- `.github/aw/campaign.md`\n- `.github/aw/charts-trending.md`\n- `.github/aw/charts.md`\n- `.github/aw/cli-commands.md`\n- `.github/aw/context.md`\n- `.github/aw/create-agentic-workflow.md`\n- `.github/aw/create-shared-agentic-workflow.md`\n- `.github/aw/debug-agentic-workflow.md`\n- `.github/aw/dependabot.md`\n- `.github/aw/deployment-status.md`\n- `.github/aw/experiments.md`\n- `.github/aw/github-agentic-workflows.md`\n- `.github/aw/github-mcp-server.md`\n- `.github/aw/llms.md`\n- `.github/aw/mcp-clis.md`\n- `.github/aw/memory.md`\n- `.github/aw/messages.md`\n- `.github/aw/network.md`\n- `.github/aw/optimize-agentic-workflow.md`\n- `.github/aw/patterns.md`\n- `.github/aw/pr-reviewer.md`\n- `.github/aw/report.md`\n- `.github/aw/reuse.md`\n- `.github/aw/safe-outputs-automation.md`\n- `.github/aw/safe-outputs-content.md`\n- `.github/aw/safe-outputs-management.md`\n- `.github/aw/safe-outputs-runtime.md`\n- `.github/aw/safe-outputs.md`\n- `.github/aw/serena-tool.md`\n- `.github/aw/shared-safe-jobs.md`\n- `.github/aw/skills.md`\n- `.github/aw/subagents.md`\n- `.github/aw/syntax-agentic.md`\n- `.github/aw/syntax-core.md`\n- `.github/aw/syntax-tools-imports.md`\n- `.github/aw/syntax.md`\n- `.github/aw/test-coverage.md`\n- `.github/aw/test-expression.md`\n- `.github/aw/token-optimization.md`\n- `.github/aw/triggers.md`\n- `.github/aw/update-agentic-workflow.md`\n- `.github/aw/upgrade-agentic-workflows.md`\n- `.github/aw/visual-regression.md`\n- `.github/aw/workflow-constraints.md`\n- `.github/aw/workflow-editing.md`\n- `.github/aw/workflow-patterns.md`\n\n- `.github/skills/agentic-workflow-designer/SKILL.md`\nAfter loading the matching workflow prompt or skill, follow it directly:\n- Design workflows from scratch via interview: `skills/agentic-workflow-designer/SKILL.md`\n- Create new workflows: `.github/aw/create-agentic-workflow.md`\n- Update existing workflows: `.github/aw/update-agentic-workflow.md`\n- Debug, audit, or investigate workflows: `.github/aw/debug-agentic-workflow.md`\n- Upgrade workflows and fix deprecations: `.github/aw/upgrade-agentic-workflows.md`\n- Create shared components or MCP wrappers: `.github/aw/create-shared-agentic-workflow.md`\n- Create report-generating workflows: `.github/aw/report.md`\n- Fix Dependabot manifest PRs: `.github/aw/dependabot.md`\n- Analyze coverage workflows: `.github/aw/test-coverage.md`\n- Render compact markdown charts: `.github/aw/asciicharts.md`\n- Map CLI commands to MCP usage: `.github/aw/cli-commands.md`\n- Choose workflow architecture and patterns: `.github/aw/patterns.md`\n- Optimize token usage and cost: `.github/aw/token-optimization.md`\n\nWhen 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 or skill.\n","frontmatter":{"name":"agentic-workflows","description":"Route gh-aw workflow design/create/debug/upgrade requests to the right prompts."},"isInternal":false,"tokens":949,"sizeBytes":3468},{"name":"SKILL.md","path":".github/skills/benchmark/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/benchmark/SKILL.md","title":"benchmark","category":"anthropic-skill","format":"markdown","content":"---\nname: benchmark\ndescription: Measure Z3 performance on a formula or file. Collects wall-clock time, theory solver statistics, memory usage, and conflict counts. Results are logged to z3agent.db for longitudinal tracking.\n---\n\nGiven an SMT-LIB2 formula or file, run Z3 with statistics enabled and report performance characteristics. This is useful for identifying performance regressions, comparing tactic strategies, and profiling theory solver workload distribution.\n\n# Step 1: Run Z3 with statistics\n\nAction:\n    Invoke benchmark.py with the formula or file. Use `--runs N` for\n    repeated timing.\n\nExpectation:\n    The script invokes `z3 -st`, parses the statistics block, and prints\n    a performance summary. A run entry is logged to z3agent.db.\n\nResult:\n    Timing and statistics are displayed. Proceed to Step 2 to interpret.\n\n```bash\npython3 scripts/benchmark.py --file problem.smt2\npython3 scripts/benchmark.py --file problem.smt2 --runs 5\npython3 scripts/benchmark.py --formula \"(declare-const x Int)...\" --debug\n```\n\n# Step 2: Interpret the output\n\nAction:\n    Review wall-clock time, memory usage, conflict counts, and per-theory\n    breakdowns.\n\nExpectation:\n    A complete performance profile including min/median/max timing when\n    multiple runs are requested.\n\nResult:\n    If performance is acceptable, no action needed.\n    If slow, try **simplify** to reduce the formula or adjust tactic strategies.\n\nThe output includes:\n\n- wall-clock time (ms)\n- result (sat/unsat/unknown/timeout)\n- memory usage (MB)\n- conflicts, decisions, propagations\n- per-theory breakdown (arithmetic, bv, array, etc.)\n\nWith `--runs N`, the script runs Z3 N times and reports min/median/max timing.\n\n# Step 3: Compare over time\n\nAction:\n    Query past benchmark runs from z3agent.db to detect regressions or\n    improvements.\n\nExpectation:\n    Historical run data is available for comparison, ordered by recency.\n\nResult:\n    If performance regressed, investigate recent formula or tactic changes.\n    If improved, record the successful configuration.\n\n```bash\npython3 ../../shared/z3db.py runs --skill benchmark --last 20\npython3 ../../shared/z3db.py query \"SELECT smtlib2, result, stats FROM formulas WHERE run_id IN (SELECT run_id FROM runs WHERE skill='benchmark') ORDER BY run_id DESC LIMIT 5\"\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula |\n| file | path | no | | path to .smt2 file |\n| runs | int | no | 1 | number of repeated runs for timing |\n| timeout | int | no | 60 | seconds per run |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n","frontmatter":{"name":"benchmark","description":"Measure Z3 performance on a formula or file. Collects wall-clock time, theory solver statistics, memory usage, and conflict counts. Results are logged to z3agent.db for longitudinal tracking."},"isInternal":false,"tokens":661,"sizeBytes":2779},{"name":"SKILL.md","path":".github/skills/encode/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/encode/SKILL.md","title":"encode","category":"anthropic-skill","format":"markdown","content":"---\nname: encode\ndescription: Translate constraint problems into SMT-LIB2 or Z3 Python API code. Handles common problem classes including scheduling, graph coloring, arithmetic puzzles, and verification conditions.\n---\n\nGiven a problem description (natural language, pseudocode, or a partial formulation), produce a complete, syntactically valid SMT-LIB2 encoding or Z3 Python script. The encoding should declare all variables, assert all constraints, and include the appropriate check-sat / get-model commands.\n\n# Step 1: Identify the problem class\n\nAction:\n    Determine the SMT theory and variable sorts required by the problem\n    description.\n\nExpectation:\n    A clear mapping from the problem to one of the supported theories\n    (LIA, LRA, QF_BV, etc.).\n\nResult:\n    If the theory is identified, proceed to Step 2. If the problem spans\n    multiple theories, select the appropriate combined logic.\n\n| Problem class | Theory | Typical sorts |\n|---------------|--------|---------------|\n| Integer arithmetic | LIA / NIA | Int |\n| Real arithmetic | LRA / NRA | Real |\n| Bitvector operations | QF_BV | (_ BitVec N) |\n| Arrays and maps | QF_AX | (Array Int Int) |\n| Strings and regex | QF_S | String, RegLan |\n| Uninterpreted functions | QF_UF | custom sorts |\n| Mixed theories | AUFLIA, etc. | combination |\n\n# Step 2: Generate the encoding\n\nAction:\n    Invoke encode.py with the problem description and desired output format.\n\nExpectation:\n    The script produces a complete SMT-LIB2 file or Z3 Python script with\n    all declarations, constraints, and check-sat commands.\n\nResult:\n    For `smtlib2` format: pass the output to **solve**.\n    For `python` format: execute the script directly.\n    Proceed to Step 3 for validation.\n\n```bash\npython3 scripts/encode.py --problem \"Find integers x, y such that x^2 + y^2 = 25 and x > 0\" --format smtlib2\npython3 scripts/encode.py --problem \"Schedule 4 tasks on 2 machines minimizing makespan\" --format python\n```\n\n# Step 3: Validate the encoding\n\nAction:\n    The script runs a syntax check by piping the output through `z3 -in`\n    in parse-only mode.\n\nExpectation:\n    No parse errors. If errors occur, the offending line is reported.\n\nResult:\n    On success: the encoding is ready for **solve**, **prove**, or **optimize**.\n    On parse error: fix the reported line and re-run.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| problem | string | yes | | problem description |\n| format | string | no | smtlib2 | output format: smtlib2 or python |\n| output | path | no | stdout | write to file instead of stdout |\n| validate | flag | no | on | run syntax check on the output |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n","frontmatter":{"name":"encode","description":"Translate constraint problems into SMT-LIB2 or Z3 Python API code. Handles common problem classes including scheduling, graph coloring, arithmetic puzzles, and verification conditions."},"isInternal":false,"tokens":679,"sizeBytes":2812},{"name":"SKILL.md","path":".github/skills/explain/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/explain/SKILL.md","title":"explain","category":"anthropic-skill","format":"markdown","content":"---\nname: explain\ndescription: Parse and interpret Z3 output for human consumption. Handles models, unsat cores, proofs, statistics, and error messages. Translates solver internals into plain-language explanations.\n---\n\nGiven raw Z3 output (from the **solve**, **prove**, **optimize**, or **benchmark** skills), produce a structured explanation. This skill is for cases where the solver output is large, nested, or otherwise difficult to read directly.\n\n# Step 1: Identify the output type\n\nAction:\n    Determine the category of Z3 output to explain: model, core,\n    statistics, error, or proof.\n\nExpectation:\n    The output type maps to one of the recognized formats in the table below.\n\nResult:\n    If the type is ambiguous, use `--type auto` and let the script detect it.\n    Proceed to Step 2.\n\n| Output contains | Explanation type |\n|----------------|-----------------|\n| `(define-fun ...)` blocks | model explanation |\n| unsat core labels | conflict explanation |\n| `:key value` statistics | performance breakdown |\n| `(error ...)` | error diagnosis |\n| proof terms | proof sketch |\n\n# Step 2: Run the explainer\n\nAction:\n    Invoke explain.py with the output file or stdin.\n\nExpectation:\n    The script auto-detects the output type and produces a structured\n    plain-language summary.\n\nResult:\n    A formatted explanation is printed. If detection fails, re-run with\n    an explicit `--type` flag.\n\n```bash\npython3 scripts/explain.py --file output.txt\npython3 scripts/explain.py --stdin < output.txt\npython3 scripts/explain.py --file output.txt --debug\n```\n\n# Step 3: Interpret the explanation\n\nAction:\n    Review the structured explanation for accuracy and completeness.\n\nExpectation:\n    Models list each variable with its value and sort. Cores list\n    conflicting assertions. Statistics show time and memory breakdowns.\n\nResult:\n    Use the explanation to answer the user query or to guide the next\n    skill invocation.\n\nFor models:\n- Each variable is listed with its value and sort\n- Array and function interpretations are expanded\n- Bitvector values are shown in decimal and hex\n\nFor unsat cores:\n- The conflicting named assertions are listed\n- A minimal conflict set is highlighted\n\nFor statistics:\n- Time breakdown by phase (preprocessing, solving, model construction)\n- Theory solver load distribution\n- Memory high-water mark\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| file | path | no | | file containing Z3 output |\n| stdin | flag | no | off | read from stdin |\n| type | string | no | auto | force output type: model, core, stats, error |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n","frontmatter":{"name":"explain","description":"Parse and interpret Z3 output for human consumption. Handles models, unsat cores, proofs, statistics, and error messages. Translates solver internals into plain-language explanations."},"isInternal":false,"tokens":607,"sizeBytes":2751},{"name":"SKILL.md","path":".github/skills/memory-safety/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/memory-safety/SKILL.md","title":"memory-safety","category":"anthropic-skill","format":"markdown","content":"---\nname: memory-safety\ndescription: Run AddressSanitizer and UndefinedBehaviorSanitizer on the Z3 test suite to detect memory errors, undefined behavior, and leaks. Logs each finding to z3agent.db.\n---\n\nBuild Z3 with compiler-based sanitizer instrumentation, execute the test suite, and parse the runtime output for memory safety violations. Supported sanitizers are AddressSanitizer (heap and stack buffer overflows, use-after-free, double-free, memory leaks) and UndefinedBehaviorSanitizer (signed integer overflow, null pointer dereference, misaligned access, shift errors). Findings are deduplicated and stored in z3agent.db for triage and longitudinal tracking.\n\n# Step 1: Configure and build\n\nAction:\n    Invoke the script with the desired sanitizer flag. The script calls\n    cmake with the appropriate `-fsanitize` flags and builds the `test-z3`\n    target. Each sanitizer uses a separate build directory to avoid flag\n    conflicts.\n\nExpectation:\n    cmake configures successfully and make compiles the instrumented binary.\n    If a prior build exists with matching flags, only incremental compilation\n    runs.\n\nResult:\n    On success: an instrumented `test-z3` binary is ready in the build\n    directory. Proceed to Step 2.\n    On failure: verify compiler support for the requested sanitizer flags\n    and review cmake output.\n\n```bash\npython3 scripts/memory_safety.py --sanitizer asan\npython3 scripts/memory_safety.py --sanitizer ubsan\npython3 scripts/memory_safety.py --sanitizer both\n```\n\nTo reuse an existing build:\n```bash\npython3 scripts/memory_safety.py --sanitizer asan --skip-build --build-dir build/sanitizer-asan\n```\n\n# Step 2: Run and collect\n\nAction:\n    Execute the instrumented test binary with halt_on_error=0 so all\n    violations are reported rather than aborting on the first.\n\nExpectation:\n    The script parses AddressSanitizer, UndefinedBehaviorSanitizer, and\n    LeakSanitizer patterns from combined output, extracts source locations,\n    and deduplicates by category/file/line.\n\nResult:\n    On `clean`: no violations detected.\n    On `findings`: one or more violations found, each printed with severity,\n    category, message, and source location.\n    On `timeout`: test suite did not finish; increase timeout or investigate.\n    On `error`: build or execution failed before sanitizer output.\n\n```bash\npython3 scripts/memory_safety.py --sanitizer asan --timeout 900 --debug\n```\n\n# Step 3: Interpret results\n\nAction:\n    Review printed findings and query z3agent.db for historical comparison.\n\nExpectation:\n    Each finding includes severity, category, message, and source location.\n    The database query returns prior runs for trend analysis.\n\nResult:\n    On `clean`: no action required; proceed.\n    On `findings`: triage by severity and category. Compare against prior\n    runs to distinguish new regressions from known issues.\n    On `timeout`: increase the deadline or investigate a possible infinite\n    loop.\n    On `error`: inspect build logs before re-running.\n\nQuery past runs:\n```bash\npython3 ../../shared/z3db.py runs --skill memory-safety --last 10\npython3 ../../shared/z3db.py query \"SELECT category, severity, file, line, message FROM findings WHERE run_id IN (SELECT run_id FROM runs WHERE skill='memory-safety') ORDER BY run_id DESC LIMIT 20\"\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| sanitizer | choice | no | asan | which sanitizer to enable: asan, ubsan, or both |\n| build-dir | path | no | build/sanitizer-{name} | path to the build directory |\n| timeout | int | no | 600 | seconds before killing the test run |\n| skip-build | flag | no | off | reuse an existing instrumented build |\n| debug | flag | no | off | verbose cmake, make, and test output |\n| db | path | no | .z3-agent/z3agent.db | path to the logging database |\n","frontmatter":{"name":"memory-safety","description":"Run AddressSanitizer and UndefinedBehaviorSanitizer on the Z3 test suite to detect memory errors, undefined behavior, and leaks. Logs each finding to z3agent.db."},"isInternal":false,"tokens":872,"sizeBytes":3872},{"name":"SKILL.md","path":".github/skills/optimize/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/optimize/SKILL.md","title":"optimize","category":"anthropic-skill","format":"markdown","content":"---\nname: optimize\ndescription: Solve constrained optimization problems using Z3. Supports minimization and maximization of objective functions over integer, real, and bitvector domains.\n---\n\nGiven a set of constraints and an objective function, find the optimal value. Z3 supports both hard constraints (must hold) and soft constraints (weighted preferences), as well as lexicographic multi-objective optimization.\n\n# Step 1: Formulate the problem\n\nAction:\n    Write constraints and an objective using `(minimize ...)` or\n    `(maximize ...)` directives, followed by `(check-sat)` and `(get-model)`.\n\nExpectation:\n    A valid SMT-LIB2 formula with at least one optimization directive and\n    all variables declared.\n\nResult:\n    If the formula is well-formed, proceed to Step 2. For multi-objective\n    problems, list directives in priority order for lexicographic optimization.\n\nExample: minimize `x + y` subject to `x >= 1`, `y >= 2`, `x + y <= 10`:\n```smtlib\n(declare-const x Int)\n(declare-const y Int)\n(assert (>= x 1))\n(assert (>= y 2))\n(assert (<= (+ x y) 10))\n(minimize (+ x y))\n(check-sat)\n(get-model)\n```\n\n# Step 2: Run the optimizer\n\nAction:\n    Invoke optimize.py with the formula or file path.\n\nExpectation:\n    The script prints `sat` with the optimal assignment, `unsat`, `unknown`,\n    or `timeout`. A run entry is logged to z3agent.db.\n\nResult:\n    On `sat`: proceed to Step 3 to read the optimal values.\n    On `unsat` or `timeout`: check constraints for contradictions or simplify.\n\n```bash\npython3 scripts/optimize.py --file scheduling.smt2\npython3 scripts/optimize.py --formula \"<inline smt-lib2>\" --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Parse the objective value and satisfying assignment from the output.\n\nExpectation:\n    `sat` with a model containing the optimal value, `unsat` indicating\n    infeasibility, or `unknown`/`timeout`.\n\nResult:\n    On `sat`: report the optimal value and assignment.\n    On `unsat`: the constraints are contradictory, no feasible solution exists.\n    On `unknown`/`timeout`: relax constraints or try **simplify**.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula with minimize/maximize |\n| file | path | no | | path to .smt2 file |\n| timeout | int | no | 60 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n","frontmatter":{"name":"optimize","description":"Solve constrained optimization problems using Z3. Supports minimization and maximization of objective functions over integer, real, and bitvector domains."},"isInternal":false,"tokens":629,"sizeBytes":2517},{"name":"SKILL.md","path":".github/skills/prove/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/prove/SKILL.md","title":"prove","category":"anthropic-skill","format":"markdown","content":"---\nname: prove\ndescription: Prove validity of logical statements by negation and satisfiability checking. If the negation is unsatisfiable, the original statement is valid. Otherwise a counterexample is returned.\n---\n\nGiven a conjecture (an SMT-LIB2 assertion or a natural language claim), determine whether it holds universally. The method is standard: negate the conjecture and check satisfiability. If the negation is unsatisfiable, the original is valid. If satisfiable, the model is a counterexample.\n\n# Step 1: Prepare the negated formula\n\nAction:\n    Wrap the conjecture in `(assert (not ...))` and append\n    `(check-sat)(get-model)`.\n\nExpectation:\n    A complete SMT-LIB2 formula that negates the original conjecture with\n    all variables declared.\n\nResult:\n    If the negation is well-formed, proceed to Step 2.\n    If the conjecture is natural language, run **encode** first.\n\nExample: to prove that `(> x 3)` implies `(> x 1)`:\n```smtlib\n(declare-const x Int)\n(assert (not (=> (> x 3) (> x 1))))\n(check-sat)\n(get-model)\n```\n\n# Step 2: Run the prover\n\nAction:\n    Invoke prove.py with the conjecture and variable declarations.\n\nExpectation:\n    The script prints `valid`, `invalid` (with counterexample), `unknown`,\n    or `timeout`. A run entry is logged to z3agent.db.\n\nResult:\n    On `valid`: proceed to **explain** if the user needs a summary.\n    On `invalid`: report the counterexample directly.\n    On `unknown`/`timeout`: try **simplify** first, or increase the timeout.\n\n```bash\npython3 scripts/prove.py --conjecture \"(=> (> x 3) (> x 1))\" --vars \"x:Int\"\n```\n\nFor file input where the file contains the full negated formula:\n```bash\npython3 scripts/prove.py --file negated.smt2\n```\n\nWith debug tracing:\n```bash\npython3 scripts/prove.py --conjecture \"(=> (> x 3) (> x 1))\" --vars \"x:Int\" --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Read the prover output to determine validity of the conjecture.\n\nExpectation:\n    One of `valid`, `invalid` (with counterexample), `unknown`, or `timeout`.\n\nResult:\n    On `valid`: the conjecture holds universally.\n    On `invalid`: the model shows a concrete counterexample.\n    On `unknown`/`timeout`: the conjecture may require auxiliary lemmas or induction.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| conjecture | string | no | | the assertion to prove (without negation) |\n| vars | string | no | | variable declarations as \"name:sort\" pairs, comma-separated |\n| file | path | no | | .smt2 file with the negated formula |\n| timeout | int | no | 30 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\nEither `conjecture` (with `vars`) or `file` must be provided.\n","frontmatter":{"name":"prove","description":"Prove validity of logical statements by negation and satisfiability checking. If the negation is unsatisfiable, the original statement is valid. Otherwise a counterexample is returned."},"isInternal":false,"tokens":735,"sizeBytes":2832},{"name":"README.md","path":".github/skills/README.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/README.md","title":"Skills Skill","category":"anthropic-skill","format":"markdown","content":"# Z3 Agent Skills\n\nReusable, composable verification primitives for the Z3 theorem prover.\nEach skill is a self-contained unit: a `SKILL.md` prompt that guides the\nLLM agent, backed by a Python validation script in `scripts/`.\n\n## Skill Catalogue\n\n| Skill | Status | Description |\n|-------|--------|-------------|\n| solve | implemented | Check satisfiability of SMT-LIB2 formulas; return models or unsat cores |\n| prove | implemented | Prove validity by negation and satisfiability checking |\n| encode | implemented | Translate constraint problems into SMT-LIB2 or Z3 Python API code |\n| simplify | implemented | Reduce formula complexity using configurable Z3 tactic chains |\n| optimize | implemented | Solve constrained optimization (minimize/maximize) over numeric domains |\n| explain | implemented | Parse and interpret Z3 output: models, cores, statistics, errors |\n| benchmark | implemented | Measure Z3 performance and collect solver statistics |\n| static-analysis | implemented | Run Clang Static Analyzer on Z3 source and log structured findings |\n| memory-safety | implemented | Run ASan/UBSan on Z3 test suite to detect memory errors and undefined behavior |\n\n## Agent\n\nA single orchestration agent composes these skills into end-to-end workflows:\n\n| Agent | Role |\n|-------|------|\n| z3 | SMT solving, code quality analysis, and stress testing |\n\n## Shared Infrastructure\n\nAll scripts share a common library at `shared/z3db.py` with:\n\n* `Z3DB`: SQLite wrapper for tracking runs, formulas, findings, and interaction logs.\n* `run_z3()`: Pipe SMT-LIB2 into `z3 -in` with timeout handling.\n* `find_z3()`: Locate the Z3 binary across build directories and PATH.\n* Parsers: `parse_model()`, `parse_stats()`, `parse_unsat_core()`.\n\nThe database schema lives in `shared/schema.sql`.\n\n## Relationship to a3/ Workflows\n\nThe `a3/` directory at the repository root contains two existing agentic workflow\nprompts that predate the skill architecture:\n\n* `a3/a3-python.md`: A3 Python Code Analysis agent (uses the a3-python pip tool\n  to scan Python source, classifies findings, creates GitHub issues).\n* `a3/a3-rust.md`: A3 Rust Verifier Output Analyzer (downloads a3-rust build\n  artifacts, parses bug reports, creates GitHub discussions).\n\nThese workflows are complementary to the skills defined here, not replaced by\nthem. The a3 prompts focus on external analysis tooling and GitHub integration,\nwhile skills focus on Z3 solver operations and their validation. Both may be\ncomposed by the same orchestrating agent.\n\n## Usage\n\nCheck database status and recent runs:\n\n```\npython shared/z3db.py status\npython shared/z3db.py runs --skill solve --last 5\npython shared/z3db.py log --run-id 12\npython shared/z3db.py query \"SELECT skill, COUNT(*) FROM runs GROUP BY skill\"\n```\n\nRun an individual skill script directly:\n\n```\npython solve/scripts/solve.py --file problem.smt2\npython encode/scripts/encode.py --validate formula.smt2\npython benchmark/scripts/benchmark.py --file problem.smt2\n```\n","isInternal":false,"tokens":686,"sizeBytes":2986},{"name":"SKILL.md","path":".github/skills/simplify/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/simplify/SKILL.md","title":"simplify","category":"anthropic-skill","format":"markdown","content":"---\nname: simplify\ndescription: Reduce formula complexity using Z3 tactic chains. Supports configurable tactic pipelines for boolean, arithmetic, and bitvector simplification.\n---\n\nGiven a formula, apply a sequence of Z3 tactics to produce an equivalent but simpler form. This is useful for understanding what Z3 sees after preprocessing, debugging tactic selection, and reducing formula size before solving.\n\n# Step 1: Choose tactics\n\nAction:\n    Select a tactic chain from the available Z3 tactics based on the\n    formula's theory.\n\nExpectation:\n    A comma-separated list of tactic names suitable for the formula domain.\n\nResult:\n    If unsure, use the default chain: `simplify,propagate-values,ctx-simplify`.\n    For bitvector formulas, add `bit-blast`. Proceed to Step 2.\n\n| Tactic | What it does |\n|--------|-------------|\n| simplify | constant folding, algebraic identities |\n| propagate-values | substitute known equalities |\n| ctx-simplify | context-dependent simplification |\n| elim-uncnstr | remove unconstrained variables |\n| solve-eqs | Gaussian elimination |\n| bit-blast | reduce bitvectors to booleans |\n| tseitin-cnf | convert to CNF |\n| aig | and-inverter graph reduction |\n\n# Step 2: Run simplification\n\nAction:\n    Invoke simplify.py with the formula and optional tactic chain.\n\nExpectation:\n    The script applies each tactic in sequence and prints the simplified\n    formula. A run entry is logged to z3agent.db.\n\nResult:\n    If the output is simpler, pass it to **solve** or **prove**.\n    If unchanged, try a different tactic chain.\n\n```bash\npython3 scripts/simplify.py --formula \"(assert (and (> x 0) (> x 0)))\" --vars \"x:Int\"\npython3 scripts/simplify.py --file formula.smt2 --tactics \"simplify,propagate-values,ctx-simplify\"\npython3 scripts/simplify.py --file formula.smt2 --debug\n```\n\nWithout `--tactics`, the script applies the default chain: `simplify`, `propagate-values`, `ctx-simplify`.\n\n# Step 3: Interpret the output\n\nAction:\n    Read the simplified formula output in SMT-LIB2 syntax.\n\nExpectation:\n    One or more `(assert ...)` blocks representing equivalent subgoals.\n\nResult:\n    A smaller formula indicates successful reduction. Pass the result to\n    **solve**, **prove**, or **optimize** as needed.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula to simplify |\n| vars | string | no | | variable declarations as \"name:sort\" pairs |\n| file | path | no | | path to .smt2 file |\n| tactics | string | no | simplify,propagate-values,ctx-simplify | comma-separated tactic names |\n| timeout | int | no | 30 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n","frontmatter":{"name":"simplify","description":"Reduce formula complexity using Z3 tactic chains. Supports configurable tactic pipelines for boolean, arithmetic, and bitvector simplification."},"isInternal":false,"tokens":673,"sizeBytes":2829},{"name":"SKILL.md","path":".github/skills/solve/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/solve/SKILL.md","title":"solve","category":"anthropic-skill","format":"markdown","content":"---\nname: solve\ndescription: Check satisfiability of SMT-LIB2 formulas using Z3. Returns sat/unsat with models or unsat cores. Logs every invocation to z3agent.db for auditability.\n---\n\nGiven an SMT-LIB2 formula (or a set of constraints described in natural language), determine whether the formula is satisfiable. If sat, extract a satisfying assignment. If unsat and tracking labels are present, extract the unsat core.\n\n# Step 1: Prepare the formula\n\nAction:\n    Convert the input to valid SMT-LIB2. If the input is natural language,\n    use the **encode** skill first.\n\nExpectation:\n    A syntactically valid SMT-LIB2 formula ending with `(check-sat)` and\n    either `(get-model)` or `(get-unsat-core)` as appropriate.\n\nResult:\n    If valid SMT-LIB2 is ready, proceed to Step 2.\n    If encoding is needed, run **encode** first and return here.\n\n# Step 2: Run Z3\n\nAction:\n    Invoke solve.py with the formula string or file path.\n\nExpectation:\n    The script pipes the formula to `z3 -in`, logs the run to\n    `.z3-agent/z3agent.db`, and prints the result.\n\nResult:\n    Output is one of `sat`, `unsat`, `unknown`, or `timeout`.\n    Proceed to Step 3 to interpret.\n\n```bash\npython3 scripts/solve.py --formula \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\"\n```\n\nFor file input:\n```bash\npython3 scripts/solve.py --file problem.smt2\n```\n\nWith debug tracing:\n```bash\npython3 scripts/solve.py --file problem.smt2 --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Parse the Z3 output to determine satisfiability and extract any model\n    or unsat core.\n\nExpectation:\n    `sat` with a model, `unsat` optionally with a core, `unknown`, or\n    `timeout`.\n\nResult:\n    On `sat`: report the model to the user.\n    On `unsat`: report the core if available.\n    On `unknown`/`timeout`: try **simplify** or increase the timeout.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula as a string |\n| file | path | no | | path to an .smt2 file |\n| timeout | int | no | 30 | seconds before killing z3 |\n| z3 | path | no | auto | explicit path to z3 binary |\n| debug | flag | no | off | print z3 command, stdin, stdout, stderr, timing |\n| db | path | no | .z3-agent/z3agent.db | path to the logging database |\n\nEither `formula` or `file` must be provided.\n","frontmatter":{"name":"solve","description":"Check satisfiability of SMT-LIB2 formulas using Z3. Returns sat/unsat with models or unsat cores. Logs every invocation to z3agent.db for auditability."},"isInternal":false,"tokens":633,"sizeBytes":2380},{"name":"SKILL.md","path":".github/skills/static-analysis/SKILL.md","rawUrl":"https://raw.githubusercontent.com/Z3Prover/z3/HEAD/.github/skills/static-analysis/SKILL.md","title":"static-analysis","category":"anthropic-skill","format":"markdown","content":"---\nname: static-analysis\ndescription: Run Clang Static Analyzer (scan-build) on Z3 source and log structured findings to z3agent.db.\n---\n\nRun the Clang Static Analyzer over a CMake build of Z3, parse the resulting plist diagnostics, and record each finding with file, line, category, and description. This skill wraps scan-build into a reproducible, logged workflow suitable for regular analysis sweeps and regression tracking.\n\n# Step 1: Run the analysis\n\nAction:\n    Invoke the script pointing at the CMake build directory. The script\n    runs `scan-build cmake -S . -B <build-dir>` followed by a scan-build-wrapped\n    `cmake --build` and writes\n    checker output to the output directory.\n\nExpectation:\n    scan-build completes within the timeout, producing plist diagnostic\n    files in the output directory (defaults to a `scan-results` subdirectory\n    of the build directory).\n\nResult:\n    On success: diagnostics are parsed and findings are printed. Proceed to\n    Step 2.\n    On failure: verify that clang and scan-build are installed and that the\n    build directory contains a valid CMake configuration.\n\n```bash\npython3 scripts/static_analysis.py --build-dir build\npython3 scripts/static_analysis.py --build-dir build --output-dir /tmp/sa-results --debug\npython3 scripts/static_analysis.py --build-dir build --timeout 1800\n```\n\n# Step 2: Interpret the output\n\nAction:\n    Review the printed findings and the summary table grouped by category.\n\nExpectation:\n    Each finding shows its source location, category, and description.\n    The summary table ranks categories by frequency for quick triage.\n\nResult:\n    On zero findings: the codebase passes all enabled static checks.\n    On findings: prioritize by category frequency and severity. Address\n    null dereferences and use-after-free classes first.\n\nExample output:\n\n```\n[Dead store] src/ast/ast.cpp:142: Value stored to 'result' is never read\n[Null dereference] src/smt/theory_lra.cpp:87: Access to field 'next' results in a dereference of a null pointer\n```\n\n# Step 3: Review historical findings\n\nAction:\n    Query z3agent.db to compare current results against prior analysis\n    runs.\n\nExpectation:\n    Queries return category counts and run history, enabling regression\n    detection across commits.\n\nResult:\n    On stable or decreasing counts: no regressions introduced.\n    On increased counts: cross-reference new findings with recent commits\n    to identify the responsible change.\n\n```bash\npython3 ../../shared/z3db.py query \"SELECT category, COUNT(*) as cnt FROM findings WHERE run_id IN (SELECT run_id FROM runs WHERE skill='static-analysis') GROUP BY category ORDER BY cnt DESC\"\npython3 ../../shared/z3db.py runs --skill static-analysis --last 10\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| build-dir | path | yes | | path to the CMake build directory |\n| output-dir | path | no | BUILD/scan-results | directory for scan-build output |\n| timeout | int | no | 1200 | seconds allowed for the full build |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n| debug | flag | no | off | verbose tracing |\n","frontmatter":{"name":"static-analysis","description":"Run Clang Static Analyzer (scan-build) on Z3 source and log structured findings to z3agent.db."},"isInternal":false,"tokens":707,"sizeBytes":3180}],"systemPromptSnippet":"<yakaai_skills repo=\"Z3Prover/z3\">\n<!-- File: .github/copilot-instructions.md (Tokens: ~1452 | Category: copilot-instructions) -->\n# Z3 Theorem Prover Development Guide\n\nAlways reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here.\n\n## Working Effectively\n\n### Bootstrap and Build the Repository\n\nZ3 is built with CMake:\n- `cmake -S . -B build` -- takes 1 second to configure\n- `cmake --build build --parallel $(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.\n\n#### Dependencies and Requirements\n- Python 3.x (required to run CMake's code generation scripts)\n- C++20 capable compiler (g++ or clang++)\n- Git (for version information)\n\n### Test the Repository\n\n- Build unit tests: `cmake --build build --target test-z3 --parallel $(nproc)` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.\n- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.\n\n**Test basic Z3 functionality:**\n```bash\n./z3 --version\necho \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\" | ./z3 -in\n```\n\n### Validation Scenarios\n\n**ALWAYS** test these scenarios after making changes:\n\n#### Basic SMT Solving\n```bash\ncd build\necho \"(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(get-model)\" | ./z3 -in\n```\nExpected output: `sat` followed by a model showing `x = 1` or similar.\n\n#### Python Bindings\n```bash\ncd build/python\npython3 -c \"import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())\"\n```\nExpected output: `Result: sat` and `Model: [x = 1]` or similar.\n\n#### Command Line Help\n```bash\n./z3 --help | head -10\n```\nShould display version and usage information.\n\n## Build System Details\n\n### CMake Build System\n- Configuration: `cmake -S . -B build` (1 second)\n- Main build: `cmake --build build --parallel $(nproc)` (17 minutes)\n- Creates Python bindings in `build/python/` when `-DZ3_BUILD_PYTHON_BINDINGS=ON` is set\n- Out-of-source build: clean build tree, no source pollution\n\n### Critical Timing and Timeout Requirements\n\n**NEVER CANCEL these operations**:\n- `cmake --build build --parallel $(nproc)`: 15-17 minutes. **Set timeout to 30+ minutes minimum**.\n- `cmake --build build --target test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**.\n- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**.\n\n**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing.\n\n## Repository Structure\n\n### Key Directories\n- `src/` - Main source code organized by components (ast, smt, sat, etc.)\n- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.)\n- `scripts/` - Build scripts and utilities\n- `.github/workflows/` - CI/CD pipeline definitions\n- `cmake/` - CMake configuration files\n\n### Important Files\n- `README.md` - Main documentation and build instructions\n- `README-CMake.md` - Detailed CMake build documentation\n- `CMakeLists.txt` - Main CMake configuration\n\n## Common Tasks and Validation\n\n### Pre-commit Validation\nBefore committing changes:\n1. **Build successfully**: Use one of the validated build commands above\n2. **Run unit tests**: `./test-z3 /a` must pass\n3. **Test basic functionality**: Run validation scenarios above\n4. **Test affected language bindings**: If modifying API, test relevant examples\n\n### Working with Language Bindings\n- **Python**: Located in `build/python/`, test with validation scenario above\n- **C/C++**: Examples in `examples/c/` and `examples/c++/`\n  - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example`\n  - Run with: `LD_LIBRARY_PATH=build ./test_example`\n- **Java**: Build with `cmake -S . -B build -DZ3_BUILD_JAVA_BINDINGS=ON`, examples in `examples/java/`\n- **C#/.NET**: Build with `cmake -S . -B build -DZ3_BUILD_DOTNET_BINDINGS=ON`, examples in `examples/dotnet/`\n\n### Performance Testing\nFor performance-sensitive changes:\n- Build optimized: `cmake -S . -B build -DCMAKE_BUILD_TYPE=Release` (Release mode)\n- Test with realistic SMT problems from `examples/SMT-LIB2/`\n- Use Z3's built-in statistics: `z3 -st problem.smt2`\n\n## Common Issues and Solutions\n\n### Python Import Errors\n- **Error**: `import z3` fails\n- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH`\n\n### Missing Dependencies\n- **Error**: Compiler not found or version too old\n- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+\n\n### Long Build Times\n- **Normal**: 15-17 minute builds are expected for Z3\n- **Never cancel**: Set timeouts appropriately and wait for completion\n- **Optimization**: Use `cmake --build build --parallel $(nproc)` for parallel compilation\n\n## Key Projects in Codebase\n\nZ3 is organized into several key components:\n\n- **Core SMT**: `src/smt/` - Main SMT solver engine\n- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver  \n- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.)\n- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation\n- **Tactics**: `src/tactic/` - Configurable solving strategies\n- **API**: `src/api/` - Public C API and language bindings\n- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers\n- **Model Generation**: Creating and manipulating satisfying assignments\n\nThe architecture is modular with clean separation between the core solver, theory plugins, and user interfaces.\n\n<!-- File: .github/skills/agentic-workflow-designer/SKILL.md (Tokens: ~4195 | Category: anthropic-skill) -->\n---\nname: agentic-workflow-designer\ndescription: Conversational skill that interviews users to design new agentic workflows\ndisable-model-invocation: true\n---\n\n# Workflow Designer\n\nUse this skill to run a structured interview with users who know their goal but not the workflow syntax yet, then generate one complete workflow `.md` file.\n\n## When to Use This Skill\n\nUse this before `.github/aw/create-agentic-workflow.md` when requirements are unclear or incomplete.\n\n- Use `skills/agentic-workflow-designer/SKILL.md` to discover and confirm requirements.\n- Use `.github/aw/create-agentic-workflow.md` once requirements are clear and ready for implementation.\n- Use `.github/aw/agentic-chat.md` when the user wants a specification/pseudo-code instead of a runnable workflow file.\n\n## Interview Framework\n\nAsk one question at a time. Move to the next phase only after the current phase is clear.\n\n### Phase 1: Goal\n\nAsk: **\"What do you want to automate?\"**\n\nCapture:\n- Workflow name (kebab-case candidate)\n- Brief description\n- Optional emoji\n\n### Phase 2: Trigger\n\nAsk: **\"When should this run?\"**\n\nFollow up only if needed:\n- Which event type(s)?\n- Any filters (labels, branches, commands)?\n- Scheduled cadence (daily/weekly/hourly)?\n\nMap to the `on:` block.\n\n### Phase 3: Scope (Read/Write)\n\nAsk:\n- **\"What should it read?\"** (issues, PRs, code, discussions, CI data)\n- **\"What should it create or update?\"** (comments, issues, PRs, labels)\n\nMap to:\n- `permissions:` (keep read-only for agent job)\n- `tools:`\n- `safe-outputs:`\n\n### Phase 4: Data Strategy\n\nAsk:\n- **\"What data does the agent need to make decisions?\"**\n- Follow up: **\"Can we pre-fetch and aggregate that data with shell commands so the agent only reads compact JSON?\"**\n\nCapture:\n- Whether `steps:` should pre-fetch GitHub data with `gh` + `jq`\n- Output paths under `/tmp/gh-aw/data/`\n- Whether batch work should use sub-agents\n\nMap to:\n- `steps:`\n- Prompt references to pre-computed file paths\n\n### Phase 5: Guardrails\n\nAsk: **\"Should it block merging, just advise, or silently log?\"**\n\nCapture:\n- Visibility expectations (comment, issue, no visible output)\n- No-op behavior expectation\n\nGuide toward safe output behavior and explicit `noop` instructions.\n\n### Phase 6: Context & Network\n\nAsk: **\"Does it need external APIs, web access, package installs, or MCP servers?\"**\n\nFollow up:\n- **\"Any third-party services or MCP servers to include (for example Slack, Jira, Datadog, custom internal MCP)?\"**\n- **\"Are you deploying on GitHub.com, GHEC with custom endpoints, or GHES?\"**\n- For each integration, identify required auth from source docs and map it to GitHub Actions secrets + workflow env variables.\n- Ask for exact external domains (FQDN/wildcard).\n\nMap to:\n- `network.allowed`\n- Optional MCP/GitHub tool usage in `tools:`\n- `secrets:` / `env:` wiring for integration tokens\n- GHES/GHEC settings such as `engine.api-target` and `aw.json` `ghes: true` (when applicable)\n\n### Phase 7: Engine (optional)\n\nAsk only if ambiguous: **\"Any AI engine preference?\"**\n\nIf no preference, suggest default:\n- \"I'd suggest Copilot since you haven't mentioned a preference. Sound good?\"\n\nMap to `engine:` only when not default.\n\n### Phase 8: Confirmation\n\nPresent a structured summary and ask for approval before generation.\n\n## Decision Heuristics\n\n### Trigger Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"when someone opens a PR\" | `on: pull_request:` with `types: [opened]` |\n| \"when a PR is updated\" | `on: pull_request:` with `types: [opened, synchronize]` |\n| \"every morning\", \"daily\" | fuzzy schedule shorthand `on: schedule: daily on weekdays` (compiler expands to cron) |\n| \"every Monday\", \"weekly\" | fuzzy schedule shorthand `on: schedule: weekly` (compiler expands to cron) |\n| \"when I say /review\" | `on: slash_command:` with `name: review` (or requested command) |\n| \"when an issue is labeled bug\" | `on: issues:` with `types: [labeled]` and label filter guidance |\n| \"run when label ai-review is added\" | `on: label_command:` with `name`/`names`, optional event scoping, and label-as-command semantics |\n| \"run on PRs from forks\" | `on: pull_request:` plus explicit `forks:` allowlist and fork security guardrails |\n| \"sometimes automatic, sometimes manual\" | semi-active pattern: combine `schedule`/event triggers with `workflow_dispatch` |\n| \"manually\", \"on demand\" | `on: workflow_dispatch:` |\n| \"when a deployment fails\" | `on: deployment_status:` |\n| \"when another workflow finishes\" | `on: workflow_run:` |\n\n### Safe Output Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"post a comment\" | `add-comment` |\n| \"create an issue\" | `create-issue` |\n| \"update issue title/body\" | `update-issue` |\n| \"close the issue\" | `close-issue` |\n| \"assign someone\", \"remove assignment\" | `assign-to-user`, `unassign-from-user` |\n| \"set issue type/field/milestone\" | `set-issue-type`, `set-issue-field`, `assign-milestone` |\n| \"open a PR\", \"submit changes\" | `create-pull-request` |\n| \"update PR description/title\" | `update-pull-request` |\n| \"close the PR\", \"merge the PR\" | `close-pull-request`, `merge-pull-request` |\n| \"mark PR ready\", \"sync PR branch\" | `mark-pull-request-as-ready-for-review`, `update-branch` |\n| \"commit a fix to the PR branch\" | `push-to-pull-request-branch` |\n| \"approve / request changes\" | `submit-pull-request-review` |\n| \"inline review comment\", \"reply to review thread\" | `create-pull-request-review-comment`, `reply-to-pull-request-review-comment`, `resolve-pull-request-review-thread` |\n| \"start or edit discussion\", \"close discussion\" | `create-discussion`, `update-discussion`, `close-discussion` |\n| \"request reviewer\", \"hide comment\" | `add-reviewer`, `hide-comment` |\n| \"create/update project\", \"project status update\" | `create-project`, `update-project`, `create-project-status-update` |\n| \"update release\", \"upload release asset\" | `update-release`, `upload-asset` |\n| \"create/auto-fix code scan alert\" | `create-code-scanning-alert`, `autofix-code-scanning-alert` |\n| \"start an agent session\", \"assign to an agent\" | `create-agent-session`, `assign-to-agent` |\n| \"store persistent memory comment\" | `comment-memory` |\n| \"link a sub-issue\" | `link-sub-issue` |\n| \"add labels\", \"remove labels\" | `add-labels`, `remove-labels` |\n| \"nothing visible\", \"just analyze\" | no safe outputs required |\n\n### Network Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"calls an external API\" | ask for exact FQDN/wildcard, then add to `network.allowed` |\n| \"reads GitHub data / clones repos\" | include `github` in `network.allowed` |\n| \"uses GitHub Actions artifacts or cache\" | include `github-actions` in `network.allowed` |\n| \"installs npm packages\" | include `node` in `network.allowed` |\n| \"runs pip install\" | include `python` in `network.allowed` |\n| \"builds Go code\" | include `go` in `network.allowed` |\n| \"installs gems / uses Bundler\" | include `ruby` in `network.allowed` |\n| \"runs cargo build\" | include `rust` in `network.allowed` |\n| \"uses NuGet / .NET restore\" | include `dotnet` in `network.allowed` |\n| \"builds with Maven / Gradle\" | include `java` in `network.allowed` |\n| \"uses Docker / pulls container images / pushes to GHCR\" | include `containers` in `network.allowed` |\n| \"runs Playwright browser tests\" | include `playwright` in `network.allowed` |\n| \"runs apt install / yum / apk\" | include `linux-distros` in `network.allowed` |\n| \"uses Terraform / HashiCorp registry\" | include `terraform` in `network.allowed` |\n| \"connects to localhost / loopback / local services\" | include `local` in `network.allowed` |\n| \"uses Swift Package Manager\" | include `swift` in `network.allowed` |\n| \"uses Composer / PHP packages\" | include `php` in `network.allowed` |\n| \"uses pub.dev / Dart packages\" | include `dart` in `network.allowed` |\n| \"uses Hackage / Haskell packages\" | include `haskell` in `network.allowed` |\n| \"uses CPAN / Perl packages\" | include `perl` in `network.allowed` |\n| \"serves or loads web fonts\" | include `fonts` in `network.allowed` |\n| \"uses Deno or JSR packages\" | include `deno` in `network.allowed` |\n| \"uses Elixir / Hex packages\" | include `elixir` in `network.allowed` |\n| \"uses Bazel build\" | include `bazel` in `network.allowed` |\n| \"uses R / CRAN packages\" | include `r` in `network.allowed` |\n| \"no external access\" | `network.allowed: [defaults]` (or `[]` if explicitly zero network) |\n\n### Tool Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"read GitHub issues/PRs/workflows\" | `tools.github` with `mode: gh-proxy` and minimal `toolsets` |\n| \"use full MCP server/tool definitions\" | `tools.github` with `mode: local` |\n| \"use other MCP servers but keep token cost down\" | `tools.cli-proxy: true` (hybrid CLI-proxy mode) |\n| \"edit files\" | `edit` tool (default unless restricted) |\n| \"run commands/tests\" | `bash` tool (default unless restricted) |\n| \"browse web pages/docs\" | `web-fetch` and/or `web-search` |\n| \"test UI flows\" | `playwright` |\n\n### Pattern Heuristics\n\n| User says... | Recommended named pattern |\n|---|---|\n| \"triage issues automatically\" | `IssueOps` |\n| \"run on /commands with human approval loops\" | `ChatOps` |\n| \"run every weekday and keep improving\" | `DailyOps` |\n| \"monitor workflow failures and trends\" | `MonitorOps` |\n| \"process a big backlog in chunks\" | `BatchOps` |\n| \"run manually with input parameters\" | `DispatchOps` |\n| \"apply a label-based workflow\" | `LabelOps` |\n| \"operate across multiple repositories\" | `MultiRepoOps` |\n| \"coordinate multiple sub-agents\" | `Orchestration` |\n| \"manage project board items\" | `ProjectOps` |\n| \"research, plan, and assign issues\" | `ResearchPlanAssignOps` |\n| \"self-correcting / retry on failure\" | `CorrectionOps` |\n| \"run in a side/fork repo\" | `SideRepoOps` |\n| \"write a spec before implementing\" | `SpecOps` |\n| \"A/B test workflow variants\" | `TrialOps` |\n| \"process items from a queue\" | `WorkQueueOps` |\n| \"deterministic, no LLM needed\" | `DeterministicOps` |\n| \"manage from a central repo\" | `CentralRepoOps` |\n| \"track work via GitHub Projects\" | `Monitoring with Projects` |\n\n### Integration Auth Mapping\n\nWhen the user names a third-party service or MCP server:\n\n1. Confirm whether native tool, MCP server, or safe-output job is the right integration path.\n2. Look up the integration's auth requirements and required scopes before finalizing the design.\n3. Provide a concrete setup checklist with:\n   - required GitHub Actions secrets (names to create)\n   - workflow env variables that consume those secrets\n   - minimum token scopes/permissions needed\n\nOutput format to use:\n\n```text\nIntegration auth setup:\n- <service-or-mcp>: <purpose>\n  - Secrets to create: <SECRET_NAME>, <SECRET_NAME>\n  - Workflow env vars: <ENV_VAR>=${{ secrets.<SECRET_NAME> }}\n  - Required scopes/permissions: <least-privilege scopes>\n```\n\nNever suggest committing plaintext tokens.\n\n### Data Strategy Mapping\n\n| User says... | Maps to |\n|---|---|\n| \"analyze PRs\", \"review issues\", \"check status\" | add `steps:` that pre-fetch with `gh` + `jq` |\n| \"read the diff\", \"look at changed files\" | add `steps:` using `gh pr diff` or `gh pr view --json files` |\n| \"search for patterns across repos\" | add `steps:` using `gh search` + `jq` filters |\n| \"just respond to a comment\" | no pre-fetch needed (event payload is enough) |\n| \"process each item individually\" | suggest sub-agent pattern with `model: small` |\n\n## Token Optimization Defaults\n\nApply these defaults unless the user explicitly asks otherwise:\n\n1. Use DataOps by default for GitHub reads: pre-fetch/aggregate with `gh` + `jq` in `steps:`, store compact JSON in `/tmp/gh-aw/data/`, and point the prompt to those files (see `.github/aw/token-optimization.md` for details).\n2. Keep tool surface minimal: default to `tools.github.mode: gh-proxy`, include only required toolsets, and prefer `bash` + `gh` for simple reads.\n3. For batch workloads, split items into compact data and suggest sub-agent processing with `model: small`.\n4. Keep prompts compact: concise imperative instructions, explicit file paths, single-line `noop` guidance, and stable instructions before dynamic content.\n\n## Progressive Disclosure Rules\n\n1. Never dump all options at once; ask one targeted question at a time.\n2. Skip questions when answers are inferable from prior user statements.\n3. Offer smart defaults and request confirmation instead of over-questioning.\n4. Ask at most 5 questions before presenting a summary; then ask \"anything else?\" if needed.\n5. Detect done signals (`that's it`, `looks good`, `generate it`) and proceed to generation.\n\n## Confirmation Format\n\nUse this exact structure:\n\n```text\n📋 Proposed workflow:\n- Name: <workflow-id>\n- Trigger: <event + key options>\n- Engine: <engine or default>\n- Tools: <tool summary>\n- Safe outputs: <list or none>\n- Network: <allowed summary>\n- Integrations/Auth: <service/mcp + required secrets/env vars>\n- Deployment: <GitHub.com or GHEC/GHES details>\n- Intent: <one-sentence task>\n```\n\nThen ask: **\"Ready to generate, or want to adjust anything?\"**\n\n## Generation Template\n\nAfter confirmation, generate one workflow file using the same skeleton style as `.github/aw/create-agentic-workflow.md`.\n\n```markdown\n---\nemoji: <emoji>\ndescription: <brief description>\non:\n  <trigger config>\npermissions:\n  contents: read\n  issues: read\n  pull-requests: read\ntools:\n  github:\n    mode: gh-proxy\n    toolsets: [default]\nsteps:\n  - name: <optional data prefetch>\n    run: |\n      mkdir -p /tmp/gh-aw/data\n      <gh + jq commands that produce compact JSON>\nsafe-outputs:\n  <safe-output-types-if-needed>\nnetwork:\n  allowed:\n    - defaults\n    - <additional entries if needed>\n---\n\n# <Workflow Name>\n\n## Task\n\n<clear instructions tied to trigger context>\nIf `steps:` includes pre-fetch commands, read the resulting `/tmp/gh-aw/data/*.json` files instead of broad live re-fetches.\n\n## Safe Outputs\n\n- Use configured safe outputs for all visible write actions.\n- Call `noop` with a short reason when no action is needed.\n```\n\n## Validation Checklist\n\nBefore final output, run this internal self-check:\n\n- [ ] Agent job permissions remain read-only (writes only via safe outputs)\n- [ ] `safe-outputs:` covers every write action mentioned in prompt/instructions\n- [ ] Network access is scoped; avoid blanket wildcard entries\n- [ ] Trigger matches the user's intended activation event\n- [ ] Prompt instructs agent to call `noop` when no action is needed\n- [ ] Unnecessary defaults are omitted (for example `engine: copilot`)\n- [ ] If reading GitHub data, `steps:` pre-fetches compact JSON (DataOps)\n- [ ] `tools.github.mode` is `gh-proxy` unless broader MCP toolsets are explicitly needed\n- [ ] Only required toolsets are listed (avoid blanket toolset lists)\n- [ ] Prompt references specific pre-computed file paths\n- [ ] For batch processing (>5 items), sub-agent pattern is suggested\n- [ ] For each third-party service/MCP integration, required secrets/env vars are listed\n- [ ] Auth guidance includes least-privilege token scope recommendations\n- [ ] For GHEC/GHES deployments, `engine.api-target` and GHES compatibility guidance are included when needed\n\n## References (load only when needed)\n\nIn-repo references:\n- `.github/aw/syntax.md` (index → `.github/aw/syntax-core.md`, `.github/aw/syntax-agentic.md`, `.github/aw/syntax-tools-imports.md`)\n- `.github/aw/safe-outputs.md` (index → `.github/aw/safe-outputs-content.md`, `.github/aw/safe-outputs-management.md`, `.github/aw/safe-outputs-automation.md`, `.github/aw/safe-outputs-runtime.md`)\n- `.github/aw/network.md`\n- `.github/aw/patterns.md`\n- `.github/aw/subagents.md`\n- `.github/aw/token-optimization.md`\n- `.github/aw/triggers.md`\n- `.github/aw/create-agentic-workflow.md`\n\nPortable HTTPS references:\n- `https://github.com/github/gh-aw/blob/main/.github/aw/syntax.md` (index → `.../syntax-core.md`, `.../syntax-agentic.md`, `.../syntax-tools-imports.md`)\n- `https://github.com/github/gh-aw/blob/main/.github/aw/safe-outputs.md` (index → `.../safe-outputs-content.md`, `.../safe-outputs-management.md`, `.../safe-outputs-automation.md`, `.../safe-outputs-runtime.md`)\n- `https://github.com/github/gh-aw/blob/main/.github/aw/network.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/patterns.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/triggers.md`\n- `https://github.com/github/gh-aw/blob/main/.github/aw/create-agentic-workflow.md`\n\n<!-- File: .github/skills/agentic-workflows/SKILL.md (Tokens: ~949 | Category: anthropic-skill) -->\n---\nname: agentic-workflows\ndescription: Route gh-aw workflow design/create/debug/upgrade requests to the right prompts.\n---\n\n# Agentic Workflows Router\n\nUse this skill when a user asks to design, create, update, debug, or upgrade GitHub Agentic Workflows in this repository.\n\nThis skill is a dispatcher: identify the task type, load the matching workflow prompt/skill file, and follow it directly. Keep responses concise and ask a clarifying question if the correct prompt is unclear.\n\nRead only the files you need:\nLoad these files from `github/gh-aw` (they are not available locally).\n- `.github/aw/agentic-chat.md`\n- `.github/aw/agentic-workflows-mcp.md`\n- `.github/aw/asciicharts.md`\n- `.github/aw/campaign.md`\n- `.github/aw/charts-trending.md`\n- `.github/aw/charts.md`\n- `.github/aw/cli-commands.md`\n- `.github/aw/context.md`\n- `.github/aw/create-agentic-workflow.md`\n- `.github/aw/create-shared-agentic-workflow.md`\n- `.github/aw/debug-agentic-workflow.md`\n- `.github/aw/dependabot.md`\n- `.github/aw/deployment-status.md`\n- `.github/aw/experiments.md`\n- `.github/aw/github-agentic-workflows.md`\n- `.github/aw/github-mcp-server.md`\n- `.github/aw/llms.md`\n- `.github/aw/mcp-clis.md`\n- `.github/aw/memory.md`\n- `.github/aw/messages.md`\n- `.github/aw/network.md`\n- `.github/aw/optimize-agentic-workflow.md`\n- `.github/aw/patterns.md`\n- `.github/aw/pr-reviewer.md`\n- `.github/aw/report.md`\n- `.github/aw/reuse.md`\n- `.github/aw/safe-outputs-automation.md`\n- `.github/aw/safe-outputs-content.md`\n- `.github/aw/safe-outputs-management.md`\n- `.github/aw/safe-outputs-runtime.md`\n- `.github/aw/safe-outputs.md`\n- `.github/aw/serena-tool.md`\n- `.github/aw/shared-safe-jobs.md`\n- `.github/aw/skills.md`\n- `.github/aw/subagents.md`\n- `.github/aw/syntax-agentic.md`\n- `.github/aw/syntax-core.md`\n- `.github/aw/syntax-tools-imports.md`\n- `.github/aw/syntax.md`\n- `.github/aw/test-coverage.md`\n- `.github/aw/test-expression.md`\n- `.github/aw/token-optimization.md`\n- `.github/aw/triggers.md`\n- `.github/aw/update-agentic-workflow.md`\n- `.github/aw/upgrade-agentic-workflows.md`\n- `.github/aw/visual-regression.md`\n- `.github/aw/workflow-constraints.md`\n- `.github/aw/workflow-editing.md`\n- `.github/aw/workflow-patterns.md`\n\n- `.github/skills/agentic-workflow-designer/SKILL.md`\nAfter loading the matching workflow prompt or skill, follow it directly:\n- Design workflows from scratch via interview: `skills/agentic-workflow-designer/SKILL.md`\n- Create new workflows: `.github/aw/create-agentic-workflow.md`\n- Update existing workflows: `.github/aw/update-agentic-workflow.md`\n- Debug, audit, or investigate workflows: `.github/aw/debug-agentic-workflow.md`\n- Upgrade workflows and fix deprecations: `.github/aw/upgrade-agentic-workflows.md`\n- Create shared components or MCP wrappers: `.github/aw/create-shared-agentic-workflow.md`\n- Create report-generating workflows: `.github/aw/report.md`\n- Fix Dependabot manifest PRs: `.github/aw/dependabot.md`\n- Analyze coverage workflows: `.github/aw/test-coverage.md`\n- Render compact markdown charts: `.github/aw/asciicharts.md`\n- Map CLI commands to MCP usage: `.github/aw/cli-commands.md`\n- Choose workflow architecture and patterns: `.github/aw/patterns.md`\n- Optimize token usage and cost: `.github/aw/token-optimization.md`\n\nWhen 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 or skill.\n\n<!-- File: .github/skills/benchmark/SKILL.md (Tokens: ~661 | Category: anthropic-skill) -->\n---\nname: benchmark\ndescription: Measure Z3 performance on a formula or file. Collects wall-clock time, theory solver statistics, memory usage, and conflict counts. Results are logged to z3agent.db for longitudinal tracking.\n---\n\nGiven an SMT-LIB2 formula or file, run Z3 with statistics enabled and report performance characteristics. This is useful for identifying performance regressions, comparing tactic strategies, and profiling theory solver workload distribution.\n\n# Step 1: Run Z3 with statistics\n\nAction:\n    Invoke benchmark.py with the formula or file. Use `--runs N` for\n    repeated timing.\n\nExpectation:\n    The script invokes `z3 -st`, parses the statistics block, and prints\n    a performance summary. A run entry is logged to z3agent.db.\n\nResult:\n    Timing and statistics are displayed. Proceed to Step 2 to interpret.\n\n```bash\npython3 scripts/benchmark.py --file problem.smt2\npython3 scripts/benchmark.py --file problem.smt2 --runs 5\npython3 scripts/benchmark.py --formula \"(declare-const x Int)...\" --debug\n```\n\n# Step 2: Interpret the output\n\nAction:\n    Review wall-clock time, memory usage, conflict counts, and per-theory\n    breakdowns.\n\nExpectation:\n    A complete performance profile including min/median/max timing when\n    multiple runs are requested.\n\nResult:\n    If performance is acceptable, no action needed.\n    If slow, try **simplify** to reduce the formula or adjust tactic strategies.\n\nThe output includes:\n\n- wall-clock time (ms)\n- result (sat/unsat/unknown/timeout)\n- memory usage (MB)\n- conflicts, decisions, propagations\n- per-theory breakdown (arithmetic, bv, array, etc.)\n\nWith `--runs N`, the script runs Z3 N times and reports min/median/max timing.\n\n# Step 3: Compare over time\n\nAction:\n    Query past benchmark runs from z3agent.db to detect regressions or\n    improvements.\n\nExpectation:\n    Historical run data is available for comparison, ordered by recency.\n\nResult:\n    If performance regressed, investigate recent formula or tactic changes.\n    If improved, record the successful configuration.\n\n```bash\npython3 ../../shared/z3db.py runs --skill benchmark --last 20\npython3 ../../shared/z3db.py query \"SELECT smtlib2, result, stats FROM formulas WHERE run_id IN (SELECT run_id FROM runs WHERE skill='benchmark') ORDER BY run_id DESC LIMIT 5\"\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula |\n| file | path | no | | path to .smt2 file |\n| runs | int | no | 1 | number of repeated runs for timing |\n| timeout | int | no | 60 | seconds per run |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\n<!-- File: .github/skills/encode/SKILL.md (Tokens: ~679 | Category: anthropic-skill) -->\n---\nname: encode\ndescription: Translate constraint problems into SMT-LIB2 or Z3 Python API code. Handles common problem classes including scheduling, graph coloring, arithmetic puzzles, and verification conditions.\n---\n\nGiven a problem description (natural language, pseudocode, or a partial formulation), produce a complete, syntactically valid SMT-LIB2 encoding or Z3 Python script. The encoding should declare all variables, assert all constraints, and include the appropriate check-sat / get-model commands.\n\n# Step 1: Identify the problem class\n\nAction:\n    Determine the SMT theory and variable sorts required by the problem\n    description.\n\nExpectation:\n    A clear mapping from the problem to one of the supported theories\n    (LIA, LRA, QF_BV, etc.).\n\nResult:\n    If the theory is identified, proceed to Step 2. If the problem spans\n    multiple theories, select the appropriate combined logic.\n\n| Problem class | Theory | Typical sorts |\n|---------------|--------|---------------|\n| Integer arithmetic | LIA / NIA | Int |\n| Real arithmetic | LRA / NRA | Real |\n| Bitvector operations | QF_BV | (_ BitVec N) |\n| Arrays and maps | QF_AX | (Array Int Int) |\n| Strings and regex | QF_S | String, RegLan |\n| Uninterpreted functions | QF_UF | custom sorts |\n| Mixed theories | AUFLIA, etc. | combination |\n\n# Step 2: Generate the encoding\n\nAction:\n    Invoke encode.py with the problem description and desired output format.\n\nExpectation:\n    The script produces a complete SMT-LIB2 file or Z3 Python script with\n    all declarations, constraints, and check-sat commands.\n\nResult:\n    For `smtlib2` format: pass the output to **solve**.\n    For `python` format: execute the script directly.\n    Proceed to Step 3 for validation.\n\n```bash\npython3 scripts/encode.py --problem \"Find integers x, y such that x^2 + y^2 = 25 and x > 0\" --format smtlib2\npython3 scripts/encode.py --problem \"Schedule 4 tasks on 2 machines minimizing makespan\" --format python\n```\n\n# Step 3: Validate the encoding\n\nAction:\n    The script runs a syntax check by piping the output through `z3 -in`\n    in parse-only mode.\n\nExpectation:\n    No parse errors. If errors occur, the offending line is reported.\n\nResult:\n    On success: the encoding is ready for **solve**, **prove**, or **optimize**.\n    On parse error: fix the reported line and re-run.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| problem | string | yes | | problem description |\n| format | string | no | smtlib2 | output format: smtlib2 or python |\n| output | path | no | stdout | write to file instead of stdout |\n| validate | flag | no | on | run syntax check on the output |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\n<!-- File: .github/skills/explain/SKILL.md (Tokens: ~607 | Category: anthropic-skill) -->\n---\nname: explain\ndescription: Parse and interpret Z3 output for human consumption. Handles models, unsat cores, proofs, statistics, and error messages. Translates solver internals into plain-language explanations.\n---\n\nGiven raw Z3 output (from the **solve**, **prove**, **optimize**, or **benchmark** skills), produce a structured explanation. This skill is for cases where the solver output is large, nested, or otherwise difficult to read directly.\n\n# Step 1: Identify the output type\n\nAction:\n    Determine the category of Z3 output to explain: model, core,\n    statistics, error, or proof.\n\nExpectation:\n    The output type maps to one of the recognized formats in the table below.\n\nResult:\n    If the type is ambiguous, use `--type auto` and let the script detect it.\n    Proceed to Step 2.\n\n| Output contains | Explanation type |\n|----------------|-----------------|\n| `(define-fun ...)` blocks | model explanation |\n| unsat core labels | conflict explanation |\n| `:key value` statistics | performance breakdown |\n| `(error ...)` | error diagnosis |\n| proof terms | proof sketch |\n\n# Step 2: Run the explainer\n\nAction:\n    Invoke explain.py with the output file or stdin.\n\nExpectation:\n    The script auto-detects the output type and produces a structured\n    plain-language summary.\n\nResult:\n    A formatted explanation is printed. If detection fails, re-run with\n    an explicit `--type` flag.\n\n```bash\npython3 scripts/explain.py --file output.txt\npython3 scripts/explain.py --stdin < output.txt\npython3 scripts/explain.py --file output.txt --debug\n```\n\n# Step 3: Interpret the explanation\n\nAction:\n    Review the structured explanation for accuracy and completeness.\n\nExpectation:\n    Models list each variable with its value and sort. Cores list\n    conflicting assertions. Statistics show time and memory breakdowns.\n\nResult:\n    Use the explanation to answer the user query or to guide the next\n    skill invocation.\n\nFor models:\n- Each variable is listed with its value and sort\n- Array and function interpretations are expanded\n- Bitvector values are shown in decimal and hex\n\nFor unsat cores:\n- The conflicting named assertions are listed\n- A minimal conflict set is highlighted\n\nFor statistics:\n- Time breakdown by phase (preprocessing, solving, model construction)\n- Theory solver load distribution\n- Memory high-water mark\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| file | path | no | | file containing Z3 output |\n| stdin | flag | no | off | read from stdin |\n| type | string | no | auto | force output type: model, core, stats, error |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\n<!-- File: .github/skills/memory-safety/SKILL.md (Tokens: ~872 | Category: anthropic-skill) -->\n---\nname: memory-safety\ndescription: Run AddressSanitizer and UndefinedBehaviorSanitizer on the Z3 test suite to detect memory errors, undefined behavior, and leaks. Logs each finding to z3agent.db.\n---\n\nBuild Z3 with compiler-based sanitizer instrumentation, execute the test suite, and parse the runtime output for memory safety violations. Supported sanitizers are AddressSanitizer (heap and stack buffer overflows, use-after-free, double-free, memory leaks) and UndefinedBehaviorSanitizer (signed integer overflow, null pointer dereference, misaligned access, shift errors). Findings are deduplicated and stored in z3agent.db for triage and longitudinal tracking.\n\n# Step 1: Configure and build\n\nAction:\n    Invoke the script with the desired sanitizer flag. The script calls\n    cmake with the appropriate `-fsanitize` flags and builds the `test-z3`\n    target. Each sanitizer uses a separate build directory to avoid flag\n    conflicts.\n\nExpectation:\n    cmake configures successfully and make compiles the instrumented binary.\n    If a prior build exists with matching flags, only incremental compilation\n    runs.\n\nResult:\n    On success: an instrumented `test-z3` binary is ready in the build\n    directory. Proceed to Step 2.\n    On failure: verify compiler support for the requested sanitizer flags\n    and review cmake output.\n\n```bash\npython3 scripts/memory_safety.py --sanitizer asan\npython3 scripts/memory_safety.py --sanitizer ubsan\npython3 scripts/memory_safety.py --sanitizer both\n```\n\nTo reuse an existing build:\n```bash\npython3 scripts/memory_safety.py --sanitizer asan --skip-build --build-dir build/sanitizer-asan\n```\n\n# Step 2: Run and collect\n\nAction:\n    Execute the instrumented test binary with halt_on_error=0 so all\n    violations are reported rather than aborting on the first.\n\nExpectation:\n    The script parses AddressSanitizer, UndefinedBehaviorSanitizer, and\n    LeakSanitizer patterns from combined output, extracts source locations,\n    and deduplicates by category/file/line.\n\nResult:\n    On `clean`: no violations detected.\n    On `findings`: one or more violations found, each printed with severity,\n    category, message, and source location.\n    On `timeout`: test suite did not finish; increase timeout or investigate.\n    On `error`: build or execution failed before sanitizer output.\n\n```bash\npython3 scripts/memory_safety.py --sanitizer asan --timeout 900 --debug\n```\n\n# Step 3: Interpret results\n\nAction:\n    Review printed findings and query z3agent.db for historical comparison.\n\nExpectation:\n    Each finding includes severity, category, message, and source location.\n    The database query returns prior runs for trend analysis.\n\nResult:\n    On `clean`: no action required; proceed.\n    On `findings`: triage by severity and category. Compare against prior\n    runs to distinguish new regressions from known issues.\n    On `timeout`: increase the deadline or investigate a possible infinite\n    loop.\n    On `error`: inspect build logs before re-running.\n\nQuery past runs:\n```bash\npython3 ../../shared/z3db.py runs --skill memory-safety --last 10\npython3 ../../shared/z3db.py query \"SELECT category, severity, file, line, message FROM findings WHERE run_id IN (SELECT run_id FROM runs WHERE skill='memory-safety') ORDER BY run_id DESC LIMIT 20\"\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| sanitizer | choice | no | asan | which sanitizer to enable: asan, ubsan, or both |\n| build-dir | path | no | build/sanitizer-{name} | path to the build directory |\n| timeout | int | no | 600 | seconds before killing the test run |\n| skip-build | flag | no | off | reuse an existing instrumented build |\n| debug | flag | no | off | verbose cmake, make, and test output |\n| db | path | no | .z3-agent/z3agent.db | path to the logging database |\n\n<!-- File: .github/skills/optimize/SKILL.md (Tokens: ~629 | Category: anthropic-skill) -->\n---\nname: optimize\ndescription: Solve constrained optimization problems using Z3. Supports minimization and maximization of objective functions over integer, real, and bitvector domains.\n---\n\nGiven a set of constraints and an objective function, find the optimal value. Z3 supports both hard constraints (must hold) and soft constraints (weighted preferences), as well as lexicographic multi-objective optimization.\n\n# Step 1: Formulate the problem\n\nAction:\n    Write constraints and an objective using `(minimize ...)` or\n    `(maximize ...)` directives, followed by `(check-sat)` and `(get-model)`.\n\nExpectation:\n    A valid SMT-LIB2 formula with at least one optimization directive and\n    all variables declared.\n\nResult:\n    If the formula is well-formed, proceed to Step 2. For multi-objective\n    problems, list directives in priority order for lexicographic optimization.\n\nExample: minimize `x + y` subject to `x >= 1`, `y >= 2`, `x + y <= 10`:\n```smtlib\n(declare-const x Int)\n(declare-const y Int)\n(assert (>= x 1))\n(assert (>= y 2))\n(assert (<= (+ x y) 10))\n(minimize (+ x y))\n(check-sat)\n(get-model)\n```\n\n# Step 2: Run the optimizer\n\nAction:\n    Invoke optimize.py with the formula or file path.\n\nExpectation:\n    The script prints `sat` with the optimal assignment, `unsat`, `unknown`,\n    or `timeout`. A run entry is logged to z3agent.db.\n\nResult:\n    On `sat`: proceed to Step 3 to read the optimal values.\n    On `unsat` or `timeout`: check constraints for contradictions or simplify.\n\n```bash\npython3 scripts/optimize.py --file scheduling.smt2\npython3 scripts/optimize.py --formula \"<inline smt-lib2>\" --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Parse the objective value and satisfying assignment from the output.\n\nExpectation:\n    `sat` with a model containing the optimal value, `unsat` indicating\n    infeasibility, or `unknown`/`timeout`.\n\nResult:\n    On `sat`: report the optimal value and assignment.\n    On `unsat`: the constraints are contradictory, no feasible solution exists.\n    On `unknown`/`timeout`: relax constraints or try **simplify**.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula with minimize/maximize |\n| file | path | no | | path to .smt2 file |\n| timeout | int | no | 60 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\n<!-- File: .github/skills/prove/SKILL.md (Tokens: ~735 | Category: anthropic-skill) -->\n---\nname: prove\ndescription: Prove validity of logical statements by negation and satisfiability checking. If the negation is unsatisfiable, the original statement is valid. Otherwise a counterexample is returned.\n---\n\nGiven a conjecture (an SMT-LIB2 assertion or a natural language claim), determine whether it holds universally. The method is standard: negate the conjecture and check satisfiability. If the negation is unsatisfiable, the original is valid. If satisfiable, the model is a counterexample.\n\n# Step 1: Prepare the negated formula\n\nAction:\n    Wrap the conjecture in `(assert (not ...))` and append\n    `(check-sat)(get-model)`.\n\nExpectation:\n    A complete SMT-LIB2 formula that negates the original conjecture with\n    all variables declared.\n\nResult:\n    If the negation is well-formed, proceed to Step 2.\n    If the conjecture is natural language, run **encode** first.\n\nExample: to prove that `(> x 3)` implies `(> x 1)`:\n```smtlib\n(declare-const x Int)\n(assert (not (=> (> x 3) (> x 1))))\n(check-sat)\n(get-model)\n```\n\n# Step 2: Run the prover\n\nAction:\n    Invoke prove.py with the conjecture and variable declarations.\n\nExpectation:\n    The script prints `valid`, `invalid` (with counterexample), `unknown`,\n    or `timeout`. A run entry is logged to z3agent.db.\n\nResult:\n    On `valid`: proceed to **explain** if the user needs a summary.\n    On `invalid`: report the counterexample directly.\n    On `unknown`/`timeout`: try **simplify** first, or increase the timeout.\n\n```bash\npython3 scripts/prove.py --conjecture \"(=> (> x 3) (> x 1))\" --vars \"x:Int\"\n```\n\nFor file input where the file contains the full negated formula:\n```bash\npython3 scripts/prove.py --file negated.smt2\n```\n\nWith debug tracing:\n```bash\npython3 scripts/prove.py --conjecture \"(=> (> x 3) (> x 1))\" --vars \"x:Int\" --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Read the prover output to determine validity of the conjecture.\n\nExpectation:\n    One of `valid`, `invalid` (with counterexample), `unknown`, or `timeout`.\n\nResult:\n    On `valid`: the conjecture holds universally.\n    On `invalid`: the model shows a concrete counterexample.\n    On `unknown`/`timeout`: the conjecture may require auxiliary lemmas or induction.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| conjecture | string | no | | the assertion to prove (without negation) |\n| vars | string | no | | variable declarations as \"name:sort\" pairs, comma-separated |\n| file | path | no | | .smt2 file with the negated formula |\n| timeout | int | no | 30 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\nEither `conjecture` (with `vars`) or `file` must be provided.\n\n<!-- File: .github/skills/README.md (Tokens: ~686 | Category: anthropic-skill) -->\n# Z3 Agent Skills\n\nReusable, composable verification primitives for the Z3 theorem prover.\nEach skill is a self-contained unit: a `SKILL.md` prompt that guides the\nLLM agent, backed by a Python validation script in `scripts/`.\n\n## Skill Catalogue\n\n| Skill | Status | Description |\n|-------|--------|-------------|\n| solve | implemented | Check satisfiability of SMT-LIB2 formulas; return models or unsat cores |\n| prove | implemented | Prove validity by negation and satisfiability checking |\n| encode | implemented | Translate constraint problems into SMT-LIB2 or Z3 Python API code |\n| simplify | implemented | Reduce formula complexity using configurable Z3 tactic chains |\n| optimize | implemented | Solve constrained optimization (minimize/maximize) over numeric domains |\n| explain | implemented | Parse and interpret Z3 output: models, cores, statistics, errors |\n| benchmark | implemented | Measure Z3 performance and collect solver statistics |\n| static-analysis | implemented | Run Clang Static Analyzer on Z3 source and log structured findings |\n| memory-safety | implemented | Run ASan/UBSan on Z3 test suite to detect memory errors and undefined behavior |\n\n## Agent\n\nA single orchestration agent composes these skills into end-to-end workflows:\n\n| Agent | Role |\n|-------|------|\n| z3 | SMT solving, code quality analysis, and stress testing |\n\n## Shared Infrastructure\n\nAll scripts share a common library at `shared/z3db.py` with:\n\n* `Z3DB`: SQLite wrapper for tracking runs, formulas, findings, and interaction logs.\n* `run_z3()`: Pipe SMT-LIB2 into `z3 -in` with timeout handling.\n* `find_z3()`: Locate the Z3 binary across build directories and PATH.\n* Parsers: `parse_model()`, `parse_stats()`, `parse_unsat_core()`.\n\nThe database schema lives in `shared/schema.sql`.\n\n## Relationship to a3/ Workflows\n\nThe `a3/` directory at the repository root contains two existing agentic workflow\nprompts that predate the skill architecture:\n\n* `a3/a3-python.md`: A3 Python Code Analysis agent (uses the a3-python pip tool\n  to scan Python source, classifies findings, creates GitHub issues).\n* `a3/a3-rust.md`: A3 Rust Verifier Output Analyzer (downloads a3-rust build\n  artifacts, parses bug reports, creates GitHub discussions).\n\nThese workflows are complementary to the skills defined here, not replaced by\nthem. The a3 prompts focus on external analysis tooling and GitHub integration,\nwhile skills focus on Z3 solver operations and their validation. Both may be\ncomposed by the same orchestrating agent.\n\n## Usage\n\nCheck database status and recent runs:\n\n```\npython shared/z3db.py status\npython shared/z3db.py runs --skill solve --last 5\npython shared/z3db.py log --run-id 12\npython shared/z3db.py query \"SELECT skill, COUNT(*) FROM runs GROUP BY skill\"\n```\n\nRun an individual skill script directly:\n\n```\npython solve/scripts/solve.py --file problem.smt2\npython encode/scripts/encode.py --validate formula.smt2\npython benchmark/scripts/benchmark.py --file problem.smt2\n```\n\n<!-- File: .github/skills/simplify/SKILL.md (Tokens: ~673 | Category: anthropic-skill) -->\n---\nname: simplify\ndescription: Reduce formula complexity using Z3 tactic chains. Supports configurable tactic pipelines for boolean, arithmetic, and bitvector simplification.\n---\n\nGiven a formula, apply a sequence of Z3 tactics to produce an equivalent but simpler form. This is useful for understanding what Z3 sees after preprocessing, debugging tactic selection, and reducing formula size before solving.\n\n# Step 1: Choose tactics\n\nAction:\n    Select a tactic chain from the available Z3 tactics based on the\n    formula's theory.\n\nExpectation:\n    A comma-separated list of tactic names suitable for the formula domain.\n\nResult:\n    If unsure, use the default chain: `simplify,propagate-values,ctx-simplify`.\n    For bitvector formulas, add `bit-blast`. Proceed to Step 2.\n\n| Tactic | What it does |\n|--------|-------------|\n| simplify | constant folding, algebraic identities |\n| propagate-values | substitute known equalities |\n| ctx-simplify | context-dependent simplification |\n| elim-uncnstr | remove unconstrained variables |\n| solve-eqs | Gaussian elimination |\n| bit-blast | reduce bitvectors to booleans |\n| tseitin-cnf | convert to CNF |\n| aig | and-inverter graph reduction |\n\n# Step 2: Run simplification\n\nAction:\n    Invoke simplify.py with the formula and optional tactic chain.\n\nExpectation:\n    The script applies each tactic in sequence and prints the simplified\n    formula. A run entry is logged to z3agent.db.\n\nResult:\n    If the output is simpler, pass it to **solve** or **prove**.\n    If unchanged, try a different tactic chain.\n\n```bash\npython3 scripts/simplify.py --formula \"(assert (and (> x 0) (> x 0)))\" --vars \"x:Int\"\npython3 scripts/simplify.py --file formula.smt2 --tactics \"simplify,propagate-values,ctx-simplify\"\npython3 scripts/simplify.py --file formula.smt2 --debug\n```\n\nWithout `--tactics`, the script applies the default chain: `simplify`, `propagate-values`, `ctx-simplify`.\n\n# Step 3: Interpret the output\n\nAction:\n    Read the simplified formula output in SMT-LIB2 syntax.\n\nExpectation:\n    One or more `(assert ...)` blocks representing equivalent subgoals.\n\nResult:\n    A smaller formula indicates successful reduction. Pass the result to\n    **solve**, **prove**, or **optimize** as needed.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula to simplify |\n| vars | string | no | | variable declarations as \"name:sort\" pairs |\n| file | path | no | | path to .smt2 file |\n| tactics | string | no | simplify,propagate-values,ctx-simplify | comma-separated tactic names |\n| timeout | int | no | 30 | seconds |\n| z3 | path | no | auto | path to z3 binary |\n| debug | flag | no | off | verbose tracing |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n\n<!-- File: .github/skills/solve/SKILL.md (Tokens: ~633 | Category: anthropic-skill) -->\n---\nname: solve\ndescription: Check satisfiability of SMT-LIB2 formulas using Z3. Returns sat/unsat with models or unsat cores. Logs every invocation to z3agent.db for auditability.\n---\n\nGiven an SMT-LIB2 formula (or a set of constraints described in natural language), determine whether the formula is satisfiable. If sat, extract a satisfying assignment. If unsat and tracking labels are present, extract the unsat core.\n\n# Step 1: Prepare the formula\n\nAction:\n    Convert the input to valid SMT-LIB2. If the input is natural language,\n    use the **encode** skill first.\n\nExpectation:\n    A syntactically valid SMT-LIB2 formula ending with `(check-sat)` and\n    either `(get-model)` or `(get-unsat-core)` as appropriate.\n\nResult:\n    If valid SMT-LIB2 is ready, proceed to Step 2.\n    If encoding is needed, run **encode** first and return here.\n\n# Step 2: Run Z3\n\nAction:\n    Invoke solve.py with the formula string or file path.\n\nExpectation:\n    The script pipes the formula to `z3 -in`, logs the run to\n    `.z3-agent/z3agent.db`, and prints the result.\n\nResult:\n    Output is one of `sat`, `unsat`, `unknown`, or `timeout`.\n    Proceed to Step 3 to interpret.\n\n```bash\npython3 scripts/solve.py --formula \"(declare-const x Int)(assert (> x 0))(check-sat)(get-model)\"\n```\n\nFor file input:\n```bash\npython3 scripts/solve.py --file problem.smt2\n```\n\nWith debug tracing:\n```bash\npython3 scripts/solve.py --file problem.smt2 --debug\n```\n\n# Step 3: Interpret the output\n\nAction:\n    Parse the Z3 output to determine satisfiability and extract any model\n    or unsat core.\n\nExpectation:\n    `sat` with a model, `unsat` optionally with a core, `unknown`, or\n    `timeout`.\n\nResult:\n    On `sat`: report the model to the user.\n    On `unsat`: report the core if available.\n    On `unknown`/`timeout`: try **simplify** or increase the timeout.\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| formula | string | no | | SMT-LIB2 formula as a string |\n| file | path | no | | path to an .smt2 file |\n| timeout | int | no | 30 | seconds before killing z3 |\n| z3 | path | no | auto | explicit path to z3 binary |\n| debug | flag | no | off | print z3 command, stdin, stdout, stderr, timing |\n| db | path | no | .z3-agent/z3agent.db | path to the logging database |\n\nEither `formula` or `file` must be provided.\n\n<!-- File: .github/skills/static-analysis/SKILL.md (Tokens: ~707 | Category: anthropic-skill) -->\n---\nname: static-analysis\ndescription: Run Clang Static Analyzer (scan-build) on Z3 source and log structured findings to z3agent.db.\n---\n\nRun the Clang Static Analyzer over a CMake build of Z3, parse the resulting plist diagnostics, and record each finding with file, line, category, and description. This skill wraps scan-build into a reproducible, logged workflow suitable for regular analysis sweeps and regression tracking.\n\n# Step 1: Run the analysis\n\nAction:\n    Invoke the script pointing at the CMake build directory. The script\n    runs `scan-build cmake -S . -B <build-dir>` followed by a scan-build-wrapped\n    `cmake --build` and writes\n    checker output to the output directory.\n\nExpectation:\n    scan-build completes within the timeout, producing plist diagnostic\n    files in the output directory (defaults to a `scan-results` subdirectory\n    of the build directory).\n\nResult:\n    On success: diagnostics are parsed and findings are printed. Proceed to\n    Step 2.\n    On failure: verify that clang and scan-build are installed and that the\n    build directory contains a valid CMake configuration.\n\n```bash\npython3 scripts/static_analysis.py --build-dir build\npython3 scripts/static_analysis.py --build-dir build --output-dir /tmp/sa-results --debug\npython3 scripts/static_analysis.py --build-dir build --timeout 1800\n```\n\n# Step 2: Interpret the output\n\nAction:\n    Review the printed findings and the summary table grouped by category.\n\nExpectation:\n    Each finding shows its source location, category, and description.\n    The summary table ranks categories by frequency for quick triage.\n\nResult:\n    On zero findings: the codebase passes all enabled static checks.\n    On findings: prioritize by category frequency and severity. Address\n    null dereferences and use-after-free classes first.\n\nExample output:\n\n```\n[Dead store] src/ast/ast.cpp:142: Value stored to 'result' is never read\n[Null dereference] src/smt/theory_lra.cpp:87: Access to field 'next' results in a dereference of a null pointer\n```\n\n# Step 3: Review historical findings\n\nAction:\n    Query z3agent.db to compare current results against prior analysis\n    runs.\n\nExpectation:\n    Queries return category counts and run history, enabling regression\n    detection across commits.\n\nResult:\n    On stable or decreasing counts: no regressions introduced.\n    On increased counts: cross-reference new findings with recent commits\n    to identify the responsible change.\n\n```bash\npython3 ../../shared/z3db.py query \"SELECT category, COUNT(*) as cnt FROM findings WHERE run_id IN (SELECT run_id FROM runs WHERE skill='static-analysis') GROUP BY category ORDER BY cnt DESC\"\npython3 ../../shared/z3db.py runs --skill static-analysis --last 10\n```\n\n# Parameters\n\n| Parameter | Type | Required | Default | Description |\n|-----------|------|----------|---------|-------------|\n| build-dir | path | yes | | path to the CMake build directory |\n| output-dir | path | no | BUILD/scan-results | directory for scan-build output |\n| timeout | int | no | 1200 | seconds allowed for the full build |\n| db | path | no | .z3-agent/z3agent.db | logging database |\n| debug | flag | no | off | verbose tracing |\n</yakaai_skills>"}