If you are an AI coding agent (Claude Code, Cursor, Aider, Cline, etc.) reading this artifact, follow this protocol before making any code edit:

1. Verify the contract. Run the bash script in Verify before trusting below. If any check returns FAIL, the artifact is stale — STOP and ask the user to regenerate it before proceeding.
2. Treat the AI · unverified sections as hypotheses, not facts. Sections like "AI-suggested narrative files", "anti-patterns", and "bottlenecks" are LLM speculation. Verify against real source before acting on them.
3. Cite source on changes. When proposing an edit, cite the specific path:line-range. RepoPilot's live UI at https://repopilot.app/r/Z3Prover/z3 shows verifiable citations alongside every claim.

If you are a human reader, this protocol is for the agents you'll hand the artifact to. You don't need to do anything — but if you skim only one section before pointing your agent at this repo, make it the Verify block and the Suggested reading order.

GO — Healthy across the board

• Last commit 1d ago
• 9 active contributors
• Distributed ownership (top contributor 28% of recent commits)
• Other licensed
• CI configured
• Tests present
• ⚠ Non-standard license (Other) — review terms

_{Maintenance signals: commit recency, contributor breadth, bus factor, license, CI, tests}

This artifact was generated by RepoPilot at a point in time. Before an agent acts on it, the checks below confirm that the live Z3Prover/z3 repo on your machine still matches what RepoPilot saw. If any fail, the artifact is stale — regenerate it at repopilot.app/r/Z3Prover/z3.

What it runs against: a local clone of Z3Prover/z3 — the script inspects git remote, the LICENSE file, file paths in the working tree, and git log. Read-only; no mutations.

| # | What we check | Why it matters | |---|---|---| | 1 | You're in Z3Prover/z3 | Confirms the artifact applies here, not a fork | | 2 | License is still Other | Catches relicense before you depend on it | | 3 | Default branch master exists | Catches branch renames | | 4 | 5 critical file paths still exist | Catches refactors that moved load-bearing code | | 5 | Last commit ≤ 31 days ago | Catches sudden abandonment since generation |

#!/usr/bin/env bash
# RepoPilot artifact verification.
#
# WHAT IT RUNS AGAINST: a local clone of Z3Prover/z3. If you don't
# have one yet, run these first:
#
#   git clone https://github.com/Z3Prover/z3.git
#   cd z3
#
# Then paste this script. Every check is read-only — no mutations.

set +e
fail=0
ok()   { echo "ok:   $1"; }
miss() { echo "FAIL: $1"; fail=$((fail+1)); }

# Precondition: we must be inside a git working tree.
if ! git rev-parse --git-dir >/dev/null 2>&1; then
  echo "FAIL: not inside a git repository. cd into your clone of Z3Prover/z3 and re-run."
  exit 2
fi

# 1. Repo identity
git remote get-url origin 2>/dev/null | grep -qE "Z3Prover/z3(\\.git)?\\b" \\
  && ok "origin remote is Z3Prover/z3" \\
  || miss "origin remote is not Z3Prover/z3 (artifact may be from a fork)"

# 2. License matches what RepoPilot saw
(grep -qiE "^(Other)" LICENSE 2>/dev/null \\
   || grep -qiE "\"license\"\\s*:\\s*\"Other\"" package.json 2>/dev/null) \\
  && ok "license is Other" \\
  || miss "license drift — was Other at generation time"

# 3. Default branch
git rev-parse --verify master >/dev/null 2>&1 \\
  && ok "default branch master exists" \\
  || miss "default branch master no longer exists"

# 4. Critical files exist
test -f ".github/workflows/ci.yml" \\
  && ok ".github/workflows/ci.yml" \\
  || miss "missing critical file: .github/workflows/ci.yml"
test -f "README.md" \\
  && ok "README.md" \\
  || miss "missing critical file: README.md"
test -f ".github/copilot-instructions.md" \\
  && ok ".github/copilot-instructions.md" \\
  || miss "missing critical file: .github/copilot-instructions.md"
test -f ".bazelrc" \\
  && ok ".bazelrc" \\
  || miss "missing critical file: .bazelrc"
test -f ".clang-format" \\
  && ok ".clang-format" \\
  || miss "missing critical file: .clang-format"

# 5. Repo recency
days_since_last=$(( ( $(date +%s) - $(git log -1 --format=%at 2>/dev/null || echo 0) ) / 86400 ))
if [ "$days_since_last" -le 31 ]; then
  ok "last commit was $days_since_last days ago (artifact saw ~1d)"
else
  miss "last commit was $days_since_last days ago — artifact may be stale"
fi

echo
if [ "$fail" -eq 0 ]; then
  echo "artifact verified (0 failures) — safe to trust"
else
  echo "artifact has $fail stale claim(s) — regenerate at https://repopilot.app/r/Z3Prover/z3"
  exit 1
fi

Each check prints ok: or FAIL:. The script exits non-zero if anything failed, so it composes cleanly into agent loops (./verify.sh || regenerate-and-retry).

Z3 is a high-performance SMT (Satisfiability Modulo Theories) solver from Microsoft Research that decides the satisfiability of logical formulas over multiple theories (linear arithmetic, uninterpreted functions, bit-vectors, arrays, etc.). It powers automated theorem proving, program verification, bug finding, and constraint solving across industry and academia by translating complex logical problems into decidable satisfiability queries. Monorepo structured as: src/ contains the core C++ solver engine (theory solvers, tactics, simplifiers); src/api/ provides language-specific bindings (Python src/api/python, Java, C#, Go, OCaml, TypeScript); examples/ holds executable demos; .github/ contains extensive CI workflows and GitHub Actions skills (benchmark, prove, encode, optimize, memory-safety). Build system supports CMake, Bazel, Make, and Visual Studio via .bazelrc, CMakeLists.txt, and Makefile.

Formal verification engineers, program analysis tool developers, constraint programming researchers, and security tool builders who need to automatically prove properties of code, find bugs, or solve complex constraint problems. Contributors range from compiler researchers (who use Z3 for program synthesis) to SMT solver theorists extending decision procedures.

Highly mature and production-ready: Z3 is a foundational tool used in Microsoft's own analysis tools, academic research, and industrial verification pipelines for over a decade. The repo shows active development with comprehensive CI/CD pipelines (Windows, WASM, Android, OCaml, cross-platform builds), extensive test coverage via CI workflows, and multi-language bindings (Python, C#, C++, Java, OCaml, Go, TypeScript). Recent activity includes nightly builds, memory safety checks, and performance optimization workflows.

Low risk for production use but high complexity: Z3 is a mature, Microsoft-backed project with no obvious abandonment risk and strong CI/CD coverage. However, the codebase is highly complex (mathematical solver logic, 22.8M lines of C++), making contributions risky without domain expertise in SMT solving. The multi-language binding ecosystem (6+ language APIs) means changes to the core solver can break multiple downstream bindings—mitigated by comprehensive cross-binding CI tests in .github/workflows/.

Active development on performance optimization (daily-perf-improver workflow in .github/actions/daily-perf-improver/), test coverage expansion (daily-test-improver with coverage tracking), and multi-platform support (Android, WASM, Pyodide, RISC-V/PowerPC builds). Recent work includes GitHub Skills for automated benchmarking, encoding, memory safety analysis, and proving—visible in .github/skills/. Pull request validation covers Windows, CI, OCaml bindings, and WASM builds.

Clone and build with CMake (primary build system):

git clone https://github.com/Z3Prover/z3.git
cd z3
mkdir build && cd build
cmake ..
make

Or using Bazel (see .bazelrc):

bazel build //src:z3

For Python bindings after build:

python -m pip install -e src/api/python

Daily commands: After build (CMake or Bazel), run the Z3 CLI directly:

./z3 --help

For Python interactive use:

python -c "from z3 import *; x = Int('x'); prove(Implies(x > 2, x > 1))"

For examples:

./build/examples/python_example  # after cmake build

Running tests:

ctest --output-on-failure  # from build/ directory

• .github/workflows/ci.yml — Main CI pipeline that validates all pull requests and commits; defines build, test, and deployment strategies across platforms.
• README.md — Entry point documentation explaining Z3's purpose, build methods, and language bindings; essential for onboarding.
• .github/copilot-instructions.md — Contributor guidelines and coding standards for the Z3 project; establishes conventions all PRs must follow.
• .bazelrc — Build configuration for Bazel, one of Z3's primary build systems; defines compiler flags and optimization settings.
• .clang-format — Code style enforcement configuration; ensures consistent formatting across the C++ and solver codebase.
• .github/workflows/release.yml — Release automation pipeline; controls how stable builds are packaged, tested, and distributed across platforms.
• .github/dependabot.yml — Dependency management configuration; monitors and automates updates for security and compatibility.

Add a new language binding

1. Create a new workflow file at .github/workflows/<language>.yml following the pattern of .github/workflows/ocaml.yaml, defining build steps and tests (.github/workflows/ocaml.yaml)
2. Add the language's build configuration in the appropriate directory (e.g., src/api/<language>/) mirroring the structure of existing bindings (.github/workflows/api-coherence-checker.lock.yml)
3. Reference the new binding in .github/copilot-instructions.md with build and testing conventions for consistency (.github/copilot-instructions.md)
4. Update .github/workflows/ci.yml to include the new language binding in the main CI pipeline (.github/workflows/ci.yml)

Add a new solver feature or tactic

1. Implement the feature following C++ formatting rules in .clang-format to ensure style compliance (.clang-format)
2. Add corresponding test cases that will be automatically run by .github/workflows/ci.yml on your PR (.github/workflows/ci.yml)
3. Run benchmarks using .github/skills/benchmark/scripts/benchmark.py to validate performance impact (.github/skills/benchmark/scripts/benchmark.py)
4. Ensure memory safety by verifying the code passes checks in .github/workflows/memory-safety.yml (.github/workflows/memory-safety.yml)

Add a new testing or validation workflow

1. Create a new workflow YAML file in .github/workflows/ following the naming convention and CI structure of .github/workflows/ci.yml (.github/workflows/ci.yml)
2. Define triggers (on push, pull_request, schedule) and jobs that execute your validation logic (.github/workflows/nightly-validation.yml)
3. If the workflow involves custom Python scripts, place them in .github/skills/<feature>/scripts/ following the pattern of existing skill scripts (.github/skills/benchmark/scripts/benchmark.py)
4. Document the workflow's purpose and maintenance in the corresponding .lock.yml file alongside .md documentation (.github/workflows/code-conventions-analyzer.lock.yml)

Add a new build target or platform

1. Create or modify the Bazel configuration in .bazelrc to support your target platform with appropriate compiler flags (.bazelrc)
2. Add a new platform-specific workflow file in .github/workflows/ (e.g., .github/workflows/custom-platform-build.yml) (.github/workflows/cross-build.yml)
3. Integrate the platform build into the release pipeline by updating .github/workflows/release.yml (.github/workflows/release.yml)
4. Ensure platform-specific code adheres to formatting rules in .clang-format and contributor guidelines in .github/copilot-instructions.md (.clang-format)

• Bazel — Multi-language build system supporting C++, OCaml, Python bindings and cross-platform compilation; enables reproducible builds and fine-grained dependency management
• GitHub Actions CI/CD — Native GitHub integration for automated testing on every PR; supports matrix builds across Windows, Linux, and specialized platforms (Android, WebAssembly)
• CMake, Make, Visual Studio — Provides alternative build paths for users with different development environments and toolchain preferences
• C++ with LLVM/Clang — Core solver engine written in C++ for performance-critical reasoning; Clang toolchain enables ASAN/MSAN memory safety validation
• Python, OCaml, Go bindings — Exposes Z3 reasoning capabilities to diverse programming ecosystems; enables integration into ML frameworks and automated verification tools

• Multiple build systems (Bazel, CMake, Make, Visual Studio, vcpkg)

  • Why: Accommodates users across different platforms and build preferences; increases accessibility
  • Consequence: Higher maintenance burden; must validate all build paths in CI; risk of configuration drift between build systems

• Extensive GitHub Actions workflows with agentic automation

  • Why: Enables sophisticated automation (code generation, optimization, analysis) and reduces manual CI maintenance
  • Consequence: Complex workflow interdependencies; harder to debug CI failures; potential for cascading failures across agentic workflows

• C++ core with bindings in multiple languages

  • Why: Maximizes performance in the solver while enabling broad ecosystem integration
  • Consequence: Bindings must stay in sync with C++ API; memory safety issues in C++ can affect all binding users; increased testing complexity

• Nightly and continuous benchmarking with performance tracking

  • Why: Prevents performance regressions and enables data-driven optimization decisions
  • Consequence: Requires maintaining benchmark infrastructure; historical data management overhead; false positives from system variance

Memory-intensive: Z3 can consume significant RAM on large problems—no explicit memory limit by default. Thread safety: Z3 contexts are not thread-safe by default; each thread needs its own context object. Solver state: Z3 maintains internal state across assert/check cycles; backtracking with push()/pop() is expensive if overused. Python GIL: Python bindings release the GIL during solver operations, but exceptions in callbacks may not propagate correctly. Build system choice: CMake and Bazel both work but have slightly different dependency handling—pick one and stick with it per project. Theory combination: Mixing incompatible theories (e.g., uninterpreted functions with array theories) can cause unexpected behavior—consult SMT theory documentation.

• SMT (Satisfiability Modulo Theories) — Z3 is fundamentally an SMT solver—you must understand what theories are (linear arithmetic, uninterpreted functions, arrays, bit-vectors, strings) and how decision procedures combine to solve formulas in their union
• DPLL(T) Algorithm — Z3's core solving strategy combines SAT solving (DPLL) with theory-specific decision procedures; understanding this framework is essential to modify or extend the solver
• Tactic Combinators — Z3's tactic system (defined in src/solver/tactic.h) is a compositional way to build problem-solving strategies—learning tactic combinators (seq, par, repeat, try) is essential for customizing the solver
• Nelson-Oppen Combination — Z3 combines multiple decision procedures (theory solvers) using Nelson-Oppen framework; understanding variable sharing and theory interface is crucial for adding new theories
• Incremental Solving and Assertion Stack — Z3 supports push()/pop() for incremental solving with backtracking; understanding the assertion stack model is critical for interactive applications and performance optimization
• E-matching and Quantifier Instantiation — Z3 uses e-matching heuristics to instantiate universally quantified formulas—this is why quantifier-heavy problems can be slow and why understanding trigger patterns matters
• AST (Abstract Syntax Tree) Representation — All formulas in Z3 are represented as ASTs with shared subterms (DAG form); understanding src/ast/ast.h is essential for any modification to formula handling or optimization

• cvc5/cvc5 — Direct competitor SMT solver with similar theory support (arithmetic, arrays, strings); users compare Z3 vs. cvc5 for performance and feature coverage
• yices2/yices2 — Alternative open-source SMT solver emphasizing efficiency; smaller codebase but narrower theory support than Z3
• seahorn/seahorn — Verification tool built on top of Z3 for C/C++ program analysis—exemplifies Z3 as a foundation for higher-level tools
• microsoft/Pex — Automated testing tool from Microsoft Research that uses Z3 internally for constraint solving and test case generation
• Microsoft/SLAM — Software Model Checking tool that pioneered SMT-based program verification techniques; spiritual predecessor to Z3's architecture

To work on one of these in Claude Code or Cursor, paste: Implement the "<title>" PR idea from CLAUDE.md, working through the checklist as the task list.

Add comprehensive Go API binding tests in src/api/go

The Go module at src/api/go is referenced in the go.mod dependencies but has no visible test coverage in the file structure. Z3 provides bindings for multiple languages, and Go is notably missing dedicated CI workflows (compare with OCaml Binding in the build status table). Adding Go-specific tests would ensure parity with other language bindings and catch regressions early.

• [ ] Create src/api/go/*_test.go files covering solver creation, assertion, and model extraction
• [ ] Add GitHub Actions workflow .github/workflows/go-bindings.yml similar to existing language-specific workflows
• [ ] Reference the existing skills framework in .github/skills/ to structure test scenarios (e.g., prove, solve, simplify)
• [ ] Document Go binding usage in a BINDING.md or update wiki with Go examples

Implement cross-platform sanitizer reporting standardization

The file .github/scripts/parse_sanitizer_reports.py exists but there's no visible corresponding sanitizer workflow automation for all platforms (Windows, Linux, macOS). The Windows.yml and other platform workflows likely run sanitizers but lack unified reporting. Creating a standardized sanitizer report aggregation system would improve code quality visibility across CI.

• [ ] Extend .github/scripts/parse_sanitizer_reports.py to handle ASAN, UBSAN, and MSAN outputs from all platforms
• [ ] Add sanitizer execution steps to .github/workflows/Windows.yml, Linux workflows, and macOS workflows
• [ ] Create a unified sanitizer report comment bot that posts results to PRs
• [ ] Add sanitizer baseline expectations to prevent regressions

Build comprehensive skill documentation and integration tests

The .github/skills/ directory contains 8 distinct skills (benchmark, encode, explain, memory-safety, optimize, prove, simplify, solve, static-analysis) but lacks cross-skill integration tests and documentation on how to chain them together. These skills appear to be AI-powered tooling for Z3 analysis, but their interaction patterns are undocumented.

• [ ] Create .github/skills/README.md with architecture overview explaining the skill framework and z3db.py shared schema
• [ ] Add integration test suite .github/skills/tests/ that verifies skill orchestration (e.g., encode → prove, simplify → optimize)
• [ ] Document each skill's input/output contract in its respective SKILL.md with concrete examples
• [ ] Add CI workflow .github/workflows/skills-integration.yml that validates all skills work together

• Add comprehensive unit tests for src/ast/expr_substitution.cpp focusing on edge cases (cyclic substitutions, variable shadowing) and benchmark performance on large ASTs—this module is frequently modified but lacks dedicated test coverage.
• Implement missing SMT-LIB 2.6 standard commands in src/parser/ (e.g., set-logic validation, declare-datatypes for recursive types)—check .github/skills/prove/scripts/prove.py for example compliance tests.
• Create TypeScript/WASM binding documentation and examples in examples/ showing how to use Z3 in browser environments—current WASM build (.github/workflows/wasm.yml) lacks user-facing tutorials.

The Z3 Theorem Prover repository has a moderate security posture. While it is an open-source academic project, there are several areas requiring attention: potential SQL injection risks in database utilities, potential secret management issues in GitHub workflows, and weak access controls on CI/CD configurations. The repository lacks visible CODEOWNERS enforcement and uses local path overrides in dependencies. The presence of multiple Python scripts in skills and GitHub actions suggests good use of automation but requires careful review to prevent injection attacks and unauthorized access. Recommendations include implementing strict secret scanning, enforcing code reviews via CODEOWNERS, auditing all workflow files, and ensuring parameterized database queries throughout.

• Medium · SQL Injection Risk in Shared Database Module — .github/skills/shared/z3db.py. The file '.github/skills/shared/z3db.py' suggests a database module that may be used across multiple skills. Without reviewing the actual code, there is potential risk of SQL injection if raw SQL queries are constructed using string interpolation or concatenation rather than parameterized queries. Fix: Review z3db.py and ensure all database queries use parameterized statements or ORM frameworks. Never concatenate user input directly into SQL queries.
• Medium · Potential Secrets in GitHub Actions Workflows — .github/workflows/ and .github/agents/. Multiple GitHub Actions workflow files and agentic workflow configurations are present. These files may contain hardcoded credentials, API keys, or sensitive environment variables if not properly managed. Fix: Audit all workflow files for hardcoded secrets. Use GitHub Secrets for sensitive data. Implement secret scanning in CI/CD pipeline. Review agentic-workflows.agent.md and z3.md for any exposed credentials.
• Low · Agentic Workflow Configuration Files Lack Access Controls — .github/agents/ and .github/aw/. The '.github/agents/' directory contains agentic workflow definitions that may be modified to alter CI/CD behavior. The presence of 'actions-lock.json' suggests an attempt at protection, but the overall security model should be reviewed. Fix: Implement strict RBAC for agentic workflow modifications. Require multi-level approvals for workflow changes. Regularly audit who has access to modify these files.
• Low · Missing CODEOWNERS Configuration — Repository root (missing file). No CODEOWNERS file is evident in the partial file structure. This could allow unauthorized modifications to critical security-sensitive areas like CI/CD configurations and build scripts. Fix: Create a CODEOWNERS file that enforces code review requirements for sensitive paths: .github/workflows/, .github/agents/, build configuration files, and security-related code.
• Low · Static Analysis Skills May Process Untrusted Code — .github/skills/static-analysis/scripts/static_analysis.py. The '.github/skills/static-analysis/' directory contains a static analysis skill. If this processes external or user-submitted code without proper sandboxing, it could be exploited for DoS or information disclosure. Fix: Implement resource limits and sandboxing for code analysis tasks. Add timeout mechanisms. Validate and sanitize input paths and code samples before processing.
• Low · Go Module Dependency with Local Path Override — go.mod (dependencies file). The go.mod file uses a 'replace' directive pointing to a local relative path '../../src/api/go'. This bypasses normal dependency resolution and version pinning, potentially introducing security risks if the local path is modified unexpectedly. Fix: Use versioned dependencies from the official repository. Document why local path overrides are necessary. Implement automated checks to ensure replace directives are only used in development and pin to specific versions in production.

LLM-derived; treat as a starting point, not a security audit.

• Open issues — current backlog
• Recent PRs — what's actively shipping
• Source on GitHub

Generated by RepoPilot. Verdict based on maintenance signals — see the live page for receipts. Re-run on a new commit to refresh.