## File: README.md

# Z3

Z3 is a theorem prover from Microsoft Research. 
It is licensed under the [MIT license](LICENSE.txt). Windows binary distributions include [C++ runtime redistributables](https://visualstudio.microsoft.com/license-terms/vs2022-cruntime/)

If you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background).

Pre-built binaries for stable and nightly releases are available [here](https://github.com/Z3Prover/z3/releases).

Z3 can be built using [Visual Studio][1], a [Makefile][2], using [CMake][3],
using [vcpkg][4], or using [Bazel][5].
It provides [bindings for several programming languages][6].

See the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3.

[](https://microsoft.github.io/z3guide/)

## Build status

### Pull Request & Push Workflows
| WASM Build | Windows Build | CI | OCaml Binding |
| ------------|---------------|----|-----------| 
| [](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/ci.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/ocaml.yaml) |

### Scheduled Workflows
| Android Build | Pyodide Wheel (PyPI) | Nightly Build | Cross Build | F* Master Build |
| ---------------|---------------|---------------|-------------|------------------|
| [](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pyodide-pypi.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/nightly.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/cross-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/fstar-master-build.yml) |

| MSVC Static | MSVC Clang-CL | Build Z3 Cache | Memory Safety | Mark PRs Ready |
|-------------|---------------|----------------|---------------|----------------|
| [](https://github.com/Z3Prover/z3/actions/workflows/msvc-static-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/msvc-static-build-clang-cl.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/build-z3-cache.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/mark-prs-ready-for-review.yml) |

### Manual & Release Workflows
| Documentation | Release Build | WASM Release |
|---------------|---------------|--------------|
| [](https://github.com/Z3Prover/z3/actions/workflows/docs.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/release.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/wasm-release.yml) |

### Specialized Workflows
| Nightly Validation | Copilot Setup | Agentics Maintenance |
|--------------------|---------------|----------------------|
| [](https://github.com/Z3Prover/z3/actions/workflows/nightly-validation.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/copilot-setup-steps.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/agentics-maintenance.yml) |

### Agentic Workflows
| API Coherence | Code Simplifier | Release Notes | Workflow Suggestion | Academic Citation |
| -------------|-----------------|---------------|---------------------|-------------------|
| [](https://github.com/Z3Prover/z3/actions/workflows/api-coherence-checker.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/code-simplifier.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/release-notes-updater.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/workflow-suggestion-agent.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/academic-citation-tracker.lock.yml) |

| Issue Backlog | Memory Safety Report | SMTLIB Benchmark Finder |
| --------------|----------------------|-------------------------|
| [](https://github.com/Z3Prover/z3/actions/workflows/issue-backlog-processor.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety-report.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/smtlib-benchmark-finder.lock.yml) |

[1]: #building-z3-on-windows-using-visual-studio-command-prompt
[2]: #building-z3-using-make-and-gccclang
[3]: #building-z3-using-cmake
[4]: #building-z3-using-vcpkg
[5]: #building-z3-using-bazel
[6]: #z3-bindings

## Building Z3 on Windows using Visual Studio Command Prompt

For 32-bit builds, start with:

```bash
python scripts/mk_make.py
```

or instead, for a 64-bit build:

```bash
python scripts/mk_make.py -x
```

then run:

```bash
cd build
nmake
```

Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019 or later.

**Security Features (MSVC)**: When building with Visual Studio/MSVC, a couple of security features are enabled by default for Z3:
- Control Flow Guard (`/guard:cf`) - enabled by default to detect attempts to compromise your code by preventing calls to locations other than function entry points, making it more difficult for attackers to execute arbitrary code through control flow redirection
- Address Space Layout Randomization (`/DYNAMICBASE`) - enabled by default for memory layout randomization, required by the `/GUARD:CF` linker option
- These can be disabled using `python scripts/mk_make.py --no-guardcf` (Python build) or `cmake -DZ3_ENABLE_CFG=OFF` (CMake build) if needed

## Building Z3 using make and GCC/Clang

Execute:

```bash
python scripts/mk_make.py
cd build
make
sudo make install
```

Note by default ``g++`` is used as C++ compiler if it is available. If you
prefer to use Clang, change the ``mk_make.py`` invocation to:

```bash
CXX=clang++ CC=clang python scripts/mk_make.py
```

Note that Clang < 3.7 does not support OpenMP.

You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler.
In that case, make sure to use Cygwin's own Python and not some Windows installation of Python.

For a 64-bit build (from Cygwin64), configure Z3's sources with
```bash
CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py
```
A 32-bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32.

By default, it will install z3 executables at ``PREFIX/bin``, libraries at
``PREFIX/lib``, and include files at ``PREFIX/include``, where the ``PREFIX``
installation prefix is inferred by the ``mk_make.py`` script. It is usually
``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and macOS. Use
the ``--prefix=`` command-line option to change the install prefix. For example:

```bash
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install
```

To uninstall Z3, use

```bash
sudo make uninstall
```

To clean Z3, you can delete the build directory and run the ``mk_make.py`` script again.

## Building Z3 using CMake

Z3 has a build system using CMake. Read the [README-CMake.md](README-CMake.md)
file for details. It is recommended for most build tasks, 
except for building OCaml bindings.

## Building Z3 using vcpkg

vcpkg is a full platform package manager. To install Z3 with vcpkg, execute:

```bash
git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3
```

## Building Z3 using Bazel

Z3 can be built using [Bazel](https://bazel.build/). This is known to work on
Ubuntu with Clang (but may work elsewhere with other compilers):
```
bazel build //...
```

## Dependencies

Z3 itself has only few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading.
It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained 
multi-precision functionality. Python is required to build Z3. Building Java, .NET, OCaml and 
Julia APIs requires installing relevant toolchains.

## Z3 bindings

Z3 has bindings for various programming languages.

### ``.NET``

You can install a NuGet package for the latest release Z3 from [nuget.org](https://www.nuget.org/packages/Microsoft.Z3/).

Use the ``--dotnet`` command line flag with ``mk_make.py`` to enable building these.

See [``examples/dotnet``](examples/dotnet) for examples.

### ``C``

These are always enabled.

See [``examples/c``](examples/c) for examples.

### ``C++``

These are always enabled.

See [``examples/c++``](examples/c++) for examples.

### ``Java``

Use the ``--java`` command line flag with ``mk_make.py`` to enable building these.

For IDE setup instructions (Eclipse, IntelliJ IDEA, Visual Studio Code) and troubleshooting, see the [Java IDE Setup Guide](doc/JAVA_IDE_SETUP.md).

See [``examples/java``](examples/java) for examples.

### ``Go``

Use the ``--go`` command line flag with ``mk_make.py`` to enable building these. Note that Go bindings use CGO and require a Go toolchain (Go 1.20 or later) to build.

With CMake, use the ``-DZ3_BUILD_GO_BINDINGS=ON`` option.

See [``examples/go``](examples/go) for examples and [``src/api/go/README.md``](src/api/go/README.md) for complete API documentation.

### ``OCaml``

Use the ``--ml`` command line flag with ``mk_make.py`` to enable building these.

See [``examples/ml``](examples/ml) for examples.

### ``Python``

You can install the Python wrapper for Z3 for the latest release from pypi using the command:

```bash
   pip install z3-solver
```

Use the ``--python`` command line flag with ``mk_make.py`` to enable building these.

Note that it is required on certain platforms that the Python package directory
(``site-packages`` on most distributions and ``dist-packages`` on Debian-based
distributions) live under the install prefix. If you use a non-standard prefix
you can use the ``--pypkgdir`` option to change the Python package directory
used for installation. For example:

```bash
python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages
```

If you do need to install to a non-standard prefix, a better approach is to use
a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/)
and install Z3 there. Python packages also work for Python3.
Under Windows, recall to build inside the Visual C++ native command build environment.
Note that the ``build/python/z3`` directory should be accessible from where Python is used with Z3 
and it requires ``libz3.dll`` to be in the path.

```bash
virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...
```

See [``examples/python``](examples/python) for examples.

### ``Julia``

The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) wraps the C API of Z3. A previous version of it wrapped the C++ API: Information about updating and building the Julia bindings can be found in [src/api/julia](src/api/julia).

### ``WebAssembly`` / ``TypeScript`` / ``JavaScript``

A WebAssembly build with associated TypeScript typings is published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver). Information about building these bindings can be found in [src/api/js](src/api/js).

### Smalltalk (``Pharo`` / ``Smalltalk/X``)

Project [MachineArithmetic](https://github.com/shingarov/MachineArithmetic) provides a Smalltalk interface
to Z3's C API. For more information, see [MachineArithmetic/README.md](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md).

### AIX

[Build settings for AIX are described here.](https://github.com/Z3Prover/z3/pull/8113)

## System Overview



## Interfaces

* Default input format is [SMTLIB2](http://smtlib.cs.uiowa.edu)

* Other native foreign function interfaces:
* [C++ API](https://z3prover.github.io/api/html/namespacez3.html)
* [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html)
* [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
* [Python API](https://z3prover.github.io/api/html/namespacez3py.html) (also available in [pydoc format](https://z3prover.github.io/api/html/z3.html))
* [Rust](https://github.com/prove-rs/z3.rs)
* C
* OCaml
* [Julia](https://github.com/ahumenberger/Z3.jl)
* [Smalltalk](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) (supports Pharo and Smalltalk/X)

## Power Tools
* The [Axiom Profiler](https://github.com/viperproject/axiom-profiler-2) currently developed by ETH Zurich

---

## File: contrib/suppressions/sanitizers/README.md

# Sanitizer suppression files

This directory contains files used to suppress
ASan/LSan/UBSan warnings/errors.

---

## File: contrib/suppressions/README.md

# Suppression files

This directory contains suppression files used by various
program analysis tools.

Suppression files tell a program analysis tool to suppress
various warnings/errors.

---

## File: doc/design_recfuns.md

# Design for handling recursive functions

Main source of inspiration is [Sutter, Köksal & Kuncak 2011],
as implemented in Leon, but the main
differences is that we should unroll function definitions directly from the
inside of Z3, in a backtracking way. Termination and fairness are ensured by
iterative-deepening on the maximum number of unrollings in a given branch.

## Unfolding

The idea is that every function definition `f(x1…xn) := rhs[x1…xn]` is
compiled into:

- a list of cases `A_f_i[x1…xn] => f(x1…xn) = rhs_i[x1…xn]`.
  When `A_f_i[t1…tn]` becomes true in the model, `f(t1…tn)` is said to be
  *unfolded* and the clause `A_f_i[t1…tn] => f(t1…tn) = rhs_i[t1…tn]`
  is added as an auxiliary clause.
- a list of constraints `Γ_f_i[x1…xn] <=> A_f_i[x1…xn]`
  that states when `A_f_i[x1…xn]` should be true, depending on inputs `x1…xn`.
  For every term `f(t1…tn)` present in congruence closure, we
  immediately add all the `Γ_f_i[t1…tn] <=> A_f_i[t1…tn]` as auxiliary clauses
  (maybe during internalization of `f(t1…tn)`?).

where each `A_f_i[x1…xn]` is a special new predicate representing the
given case of `f`, and `rhs_i` does not contain any `ite`.
We assume pattern matching has been compiled to `ite` beforehand.

For example, `fact(n) := if n<2 then 1 else n * fact(n-1)` is compiled into:

- `A_fact_0[n] => fact(n) = 1`
- `A_fact_1[n] => fact(n) = n * fact(n-1)`
- `A_fact_0[n] <=> n < 2`
- `A_fact_1[n] <=> ¬(n < 2)`

The 2 first clauses are only added when `A_fact_0[t]` is true
(respectively `A_fact_1[t]` is true).
The 2 other clauses are added as soon as `fact(t)` is internalized.

## Termination

To ensure termination, we define variables:

- `unfold_depth: int`
- `current_max_unfold_depth: int`
- `global_max_unfold_depth: int`

and a special literal `[max_depth=$n]` for each `n:int`.
Solving is done under the local assumption
`[max_depth=$current_max_unfold_depth]` (this should be handled in some outer
loop, e.g. in a custom tactic).

Whenever `A_f_i[t1…tn]` becomes true (for any `f`), we increment
`unfold_depth`. If `unfold_depth > current_max_unfold_depth`, then
the conflict clause `[max_depth=$current_max_unfold_depth] => Γ => false`
where `Γ` is the conjunction of all `A_f_i[t1…tn]` true in the trail.

For non-recursive functions, we don't have to increment `unfold_depth`. Some other functions that are known

If the solver answers "SAT", we have a model.
Otherwise, if `[max_depth=$current_max_unfold_depth]` is part of the
unsat-core, then we increase `current_max_unfold_depth`.
If `current_max_unfold_depth == global_max_unfold_depth` then
we report "UNKNOWN" (reached global depth limit), otherwise we can
try to `solve()` again with the new assumption (higher depth limit).

## Tactic

there should be a parametrized tactic `funrec(t, n)` where `t` is the tactic
used to solve (under assumption that depth is limited to `current_max_unfold_depth`)
and `n` is an integer that is assigned to `global_max_unfold_depth`.

This way, to try and find models for a problem with recursive functions + LIA,
one could use something like `(funrec (then simplify dl smt) 100)`.

## Expected benefits

This addition to Z3 would bring many benefits compared to current alternatives (Leon, quantifiers, …)

- should be very fast and lightweight
  (compared to Leon or quantifiers).
  In particular, every function call is very lightweight even compared to Leon (no need for full model building, followed by unsat core extraction)
- possibility of answering "SAT" for any `QF_*` fragment +
  recursive functions
- makes `define-funs-rec` a first-class citizen of the language,  usable to model user-defined theories or to analyze functional
  programs directly

## Optimizations

- maybe `C_f_i` literals should never be decided on
  (they can always be propagated).
  Even stronger: they should not be part of conflicts?
  (i.e. tune conflict resolution to always resolve
   these literals away, disregarding their level)

---

## File: doc/JAVA_IDE_SETUP.md

# Z3 Java Bindings: IDE Setup Guide

This guide explains how to set up and use Z3 Java bindings in popular Java IDEs (Eclipse, IntelliJ IDEA, and Visual Studio Code).

## Prerequisites

Before setting up Z3 in your IDE, you need to obtain the Z3 binaries:

### Option 1: Download Pre-built Binaries (Recommended)

1. Download the appropriate Z3 release for your platform from the [Z3 Releases page](https://github.com/Z3Prover/z3/releases)
   - For Windows: `z3-x.x.x-x64-win.zip`
   - For Linux: `z3-x.x.x-x64-glibc-x.x.zip`
   - For macOS: `z3-x.x.x-x64-osx-x.x.zip`

2. Extract the archive to a location on your system (e.g., `C:\z3` on Windows or `/opt/z3` on Linux/macOS)

3. The extracted folder contains:
   - `bin/com.microsoft.z3.jar` - The Java API library
   - `bin/libz3.dll` (Windows) / `bin/libz3.so` (Linux) / `bin/libz3.dylib` (macOS) - The native Z3 library
   - `bin/libz3java.dll` (Windows) / `bin/libz3java.so` (Linux) / `bin/libz3java.dylib` (macOS) - The Java JNI bridge

### Option 2: Build from Source

If you need to build Z3 from source with Java bindings enabled:

```bash
python scripts/mk_make.py --java
cd build
make
```

The resulting files will be in the `build` directory.

## Eclipse Setup

### Step 1: Add Z3 JAR to Build Path

1. Right-click on your Java project in the **Package Explorer**
2. Select **Build Path** → **Configure Build Path...**
3. In the **Libraries** tab, click **Add External JARs...**
4. Navigate to the Z3 `bin` folder and select `com.microsoft.z3.jar`
5. Click **Apply and Close**

### Step 2: Configure Native Library Path

Eclipse needs to know where to find the native Z3 libraries (`.dll`, `.so`, or `.dylib` files).

**Method 1: Using Eclipse Native Library Location (Recommended)**

1. In the **Package Explorer**, expand the **Referenced Libraries** section
2. Find and expand `com.microsoft.z3.jar`
3. Right-click on **Native Library Location** and select **Edit...**
4. Click **External Folder...** and select the Z3 `bin` folder (where the native libraries are located)
5. Click **OK**

**Method 2: Using VM Arguments**

1. Right-click on your project → **Run As** → **Run Configurations...**
2. Select your Java application configuration (or create a new one)
3. Go to the **Arguments** tab
4. In the **VM arguments** field, add:
   ```
   -Djava.library.path=C:\path\to\z3\bin
   ```
   (Replace with your actual Z3 bin directory path)
5. Click **Apply** and **Run**

**Method 3: Using System PATH (Windows)**

1. Add the Z3 `bin` directory to your system PATH environment variable:
   - Open **System Properties** → **Advanced** → **Environment Variables**
   - Under **System Variables**, find and edit the `Path` variable
   - Add the full path to your Z3 `bin` directory (e.g., `C:\z3\bin`)
   - Click **OK** and restart Eclipse

### Step 3: Verify Setup

Create a test Java file with the following code:

```java
import com.microsoft.z3.*;

public class Z3Test {
    public static void main(String[] args) {
        System.out.println("Creating Z3 context...");
        Context ctx = new Context();
        System.out.println("Z3 version: " + Version.getFullVersion());
        
        // Simple example: x > 0
        IntExpr x = ctx.mkIntConst("x");
        Solver solver = ctx.mkSolver();
        solver.add(ctx.mkGt(x, ctx.mkInt(0)));
        
        if (solver.check() == Status.SATISFIABLE) {
            System.out.println("SAT");
            System.out.println("Model: " + solver.getModel());
        }
        
        ctx.close();
        System.out.println("Success!");
    }
}
```

Run the program. If you see the Z3 version and "Success!" printed, your setup is working correctly.

## IntelliJ IDEA Setup

### Step 1: Add Z3 JAR to Project

1. Open your project in IntelliJ IDEA
2. Go to **File** → **Project Structure** (or press `Ctrl+Alt+Shift+S`)
3. Select **Modules** → **Dependencies**
4. Click the **+** button and select **JARs or directories...**
5. Navigate to the Z3 `bin` folder and select `com.microsoft.z3.jar`
6. Click **OK** and **Apply**

### Step 2: Configure Native Library Path

**Method 1: Using Run Configuration (Recommended)**

1. Go to **Run** → **Edit Configurations...**
2. Select your application configuration (or create a new one)
3. In the **VM options** field, add:
   ```
   -Djava.library.path=/path/to/z3/bin
   ```
   (Replace with your actual Z3 bin directory path)
4. Click **OK**

**Method 2: Using Environment Variable (Windows)**

Add the Z3 `bin` directory to your system PATH as described in the Eclipse section above, then restart IntelliJ IDEA.

### Step 3: Verify Setup

Use the same test code from the Eclipse section to verify your setup.

## Visual Studio Code Setup

### Step 1: Install Java Extension Pack

1. Open Visual Studio Code
2. Install the **Extension Pack for Java** from the Extensions marketplace

### Step 2: Add Z3 JAR to Classpath

Create or edit `.vscode/settings.json` in your project root:

```json
{
    "java.project.referencedLibraries": [
        "path/to/z3/bin/com.microsoft.z3.jar"
    ]
}
```

### Step 3: Configure Native Library Path

Create or edit `.vscode/launch.json` in your project root:

```json
{
    "version": "0.2.0",
    "configurations": [
        {
            "type": "java",
            "name": "Launch with Z3",
            "request": "launch",
            "mainClass": "YourMainClass",
            "vmArgs": "-Djava.library.path=/path/to/z3/bin"
        }
    ]
}
```

Replace `YourMainClass` with your actual main class name and adjust the path to your Z3 bin directory.

### Step 4: Verify Setup

Use the same test code to verify your setup.

## Command-Line Build and Run

If you prefer to build and run from the command line:

### Compiling

```bash
# Windows
javac -cp "C:\path\to\z3\bin\com.microsoft.z3.jar;." YourProgram.java

# Linux/macOS
javac -cp "/path/to/z3/bin/com.microsoft.z3.jar:." YourProgram.java
```

### Running

```bash
# Windows
java -cp "C:\path\to\z3\bin\com.microsoft.z3.jar;." -Djava.library.path=C:\path\to\z3\bin YourProgram

# Linux
LD_LIBRARY_PATH=/path/to/z3/bin java -cp "/path/to/z3/bin/com.microsoft.z3.jar:." YourProgram

# macOS
DYLD_LIBRARY_PATH=/path/to/z3/bin java -cp "/path/to/z3/bin/com.microsoft.z3.jar:." YourProgram
```

## Troubleshooting

### ClassNotFoundException: com.microsoft.z3.Context

**Problem:** Java cannot find the Z3 classes.

**Solution:**
- Verify that `com.microsoft.z3.jar` is in your project's classpath
- In Eclipse: Check **Project Properties** → **Java Build Path** → **Libraries**
- In IntelliJ: Check **File** → **Project Structure** → **Modules** → **Dependencies**
- Ensure you're not just copying the JAR to your project's bin folder - it must be explicitly added to the classpath

### UnsatisfiedLinkError: no z3java in java.library.path

**Problem:** Java can find the Z3 classes but cannot load the native libraries.

**Solution:**
- Verify that `libz3.dll`/`libz3.so`/`libz3.dylib` and `libz3java.dll`/`libz3java.so`/`libz3java.dylib` are in a directory accessible to Java
- Add the Z3 `bin` directory to:
  - The `java.library.path` VM argument, or
  - The system PATH environment variable (Windows), or
  - The LD_LIBRARY_PATH (Linux) / DYLD_LIBRARY_PATH (macOS) environment variable

### ExceptionInInitializerError or Z3Exception

**Problem:** Z3 fails to initialize properly.

**Solution:**
- Ensure all Z3 files (JAR and native libraries) are from the same version
- Check that you're using a compatible Java version (Java 8 or later)
- Verify that the native libraries match your system architecture (32-bit vs 64-bit)

### Running on Different Platforms

**Windows:**
- Use semicolons (`;`) as classpath separators
- Native libraries: `libz3.dll` and `libz3java.dll`
- Set PATH or use `-Djava.library.path`

**Linux:**
- Use colons (`:`) as classpath separators  
- Native libraries: `libz3.so` and `libz3java.so`
- Set LD_LIBRARY_PATH or use `-Djava.library.path`

**macOS:**
- Use colons (`:`) as classpath separators
- Native libraries: `libz3.dylib` and `libz3java.dylib`
- Set DYLD_LIBRARY_PATH or use `-Djava.library.path`

## Maven/Gradle Setup

For Maven or Gradle projects, you can use system-scoped dependencies:

### Maven

```xml
<dependency>
    <groupId>com.microsoft</groupId>
    <artifactId>z3</artifactId>
    <version>x.x.x</version> 
    <scope>system</scope>
    <systemPath>${project.basedir}/lib/com.microsoft.z3.jar</systemPath>
</dependency>
```

Place the Z3 JAR in your project's `lib` directory and configure the native library path as described above.

### Gradle

```gradle
dependencies {
    implementation files('lib/com.microsoft.z3.jar')
}
```

## Additional Resources

- [Z3 GitHub Repository](https://github.com/Z3Prover/z3)
- [Z3 Java API Documentation](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
- [Z3 Examples](https://github.com/Z3Prover/z3/tree/master/examples/java)
- [Z3 Guide](https://microsoft.github.io/z3guide/)

## Building Z3 with Java Support

If you need to build Z3 from source with Java bindings:

```bash
# Clone the repository
git clone https://github.com/Z3Prover/z3.git
cd z3

# Configure with Java support
python scripts/mk_make.py --java

# Build
cd build
make

# The Java bindings will be in the build directory
# - com.microsoft.z3.jar
# - libz3java.so / libz3java.dll / libz3java.dylib
# - libz3.so / libz3.dll / libz3.dylib
```

For more details on building Z3, see the main [README.md](../README.md).

---

## File: examples/go/README.md

# Z3 Go Examples

This directory contains examples demonstrating how to use the Z3 Go bindings.

## Examples

### basic_example.go

Demonstrates fundamental Z3 operations:
- Creating contexts and solvers
- Defining integer and boolean variables
- Adding constraints
- Checking satisfiability
- Extracting models

## Building and Running

### Prerequisites

1. Build Z3 with Go bindings enabled
2. Ensure Z3 library is in your library path
3. Go 1.20 or later

### Linux/macOS

```bash
# Build Z3 first
cd ../..
mkdir build && cd build
cmake ..
make -j$(nproc)

# Set up environment
cd ../examples/go
export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
export CGO_CFLAGS="-I../../src/api"
export CGO_LDFLAGS="-L../../build -lz3"

# Run examples
go run basic_example.go
```

### Windows

```cmd
REM Build Z3 first
cd ..\..
mkdir build
cd build
cmake ..
cmake --build . --config Release

REM Set up environment
cd ..\examples\go
set PATH=..\..\build\Release;%PATH%
set CGO_CFLAGS=-I..\..\src\api
set CGO_LDFLAGS=-L..\..\build\Release -lz3

REM Run examples
go run basic_example.go
```

## Expected Output

When you run `basic_example.go`, you should see output similar to:

```
Z3 Go Bindings - Basic Example
================================

Example 1: Solving x > 0
Satisfiable!
Model: ...
x = 1

Example 2: Solving x + y = 10 ∧ x - y = 2
Satisfiable!
x = 6
y = 4

Example 3: Boolean satisfiability
Satisfiable!
p = false
q = true

Example 4: Checking unsatisfiability
Status: unsat
The constraints are unsatisfiable (as expected)

All examples completed successfully!
```

## Creating Your Own Examples

1. Import the Z3 package:
   ```go
   import "github.com/Z3Prover/z3/src/api/go"
   ```

2. Create a context:
   ```go
   ctx := z3.NewContext()
   ```

3. Create variables and constraints:
   ```go
   x := ctx.MkIntConst("x")
   constraint := ctx.MkGt(x, ctx.MkInt(0, ctx.MkIntSort()))
   ```

4. Solve:
   ```go
   solver := ctx.NewSolver()
   solver.Assert(constraint)
   if solver.Check() == z3.Satisfiable {
       model := solver.Model()
       // Use model...
   }
   ```

## Troubleshooting

### "undefined reference to Z3_*" errors

Make sure:
- Z3 is built and the library is in your library path
- CGO_LDFLAGS includes the correct library path
- On Windows, the DLL is in your PATH

### "cannot find package" errors

Make sure:
- CGO_CFLAGS includes the Z3 API header directory
- The go.mod file exists in src/api/go

### CGO compilation errors

Ensure:
- CGO is enabled (set CGO_ENABLED=1 if needed)
- You have a C compiler installed (gcc, clang, or MSVC)
- The Z3 headers are accessible

## More Information

See the README.md in src/api/go for complete API documentation.

---

## File: examples/python/tutorial/jupyter/README.md

# Jupyter version of the Z3 Python Tutorial.

Thanks to Peter Gragert, the Z3 tutorial guide is now available in the Jupyter notebook format. 

An online tutorial is available from https://github.com/philzook58/z3_tutorial

---

## File: src/api/dotnet/README.md

# Z3 Nuget Package

For more information see [the Z3 github page](https://github.com/z3prover/z3.git)

---

## File: src/api/go/README.md

# Z3 Go Bindings

This directory contains Go language bindings for the Z3 theorem prover.

## Overview

The Go bindings provide a comprehensive interface to Z3's C API using CGO. The bindings support:

- **Core Z3 Types**: Context, Config, Symbol, AST, Sort, Expr, FuncDecl
- **Solver Operations**: Creating solvers, asserting constraints, checking satisfiability
- **Model Manipulation**: Extracting and evaluating models
- **Boolean Logic**: And, Or, Not, Implies, Iff, Xor
- **Arithmetic**: Add, Sub, Mul, Div, Mod, comparison operators
- **Bit-vectors**: Full bit-vector arithmetic, bitwise operations, shifts, comparisons
- **Floating Point**: IEEE 754 floating-point arithmetic with rounding modes
- **Arrays**: Select, Store, constant arrays
- **Sequences/Strings**: String operations, concatenation, contains, indexing
- **Regular Expressions**: Pattern matching, Kleene star/plus, regex operations
- **Quantifiers**: Forall, Exists
- **Functions**: Function declarations and applications
- **Tactics & Goals**: Goal-based solving and tactic combinators
- **Probes**: Goal property checking
- **Datatypes**: Algebraic datatypes, tuples, enumerations, lists
- **Parameters**: Solver and tactic configuration
- **Optimize**: Optimization problems with maximize/minimize objectives

## Building

### Prerequisites

- Go 1.20 or later
- Z3 library built and installed
- CGO enabled

### With CMake

```bash
mkdir build && cd build
cmake -DBUILD_GO_BINDINGS=ON ..
make
```

### With Python Build System

```bash
python scripts/mk_make.py --go
cd build
make
```

## Usage

### Basic Example

```go
package main

import (
    "fmt"
    "github.com/Z3Prover/z3/src/api/go"
)

func main() {
    // Create a context
    ctx := z3.NewContext()
    
    // Create variables
    x := ctx.MkIntConst("x")
    y := ctx.MkIntConst("y")
    
    // Create constraints: x + y == 10 && x > y
    ten := ctx.MkInt(10, ctx.MkIntSort())
    eq := ctx.MkEq(ctx.MkAdd(x, y), ten)
    gt := ctx.MkGt(x, y)
    
    // Create solver and check
    solver := ctx.NewSolver()
    solver.Assert(eq)
    solver.Assert(gt)
    
    if solver.Check() == z3.Satisfiable {
        model := solver.Model()
        if xVal, ok := model.Eval(x, true); ok {
            fmt.Println("x =", xVal.String())
        }
        if yVal, ok := model.Eval(y, true); ok {
            fmt.Println("y =", yVal.String())
        }
    }
}
```

### Running Examples

```bash
cd examples/go

# Set library path (Linux/Mac)
export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
export CGO_CFLAGS="-I../../src/api"
export CGO_LDFLAGS="-L../../build -lz3"

# Set library path (Windows)
set PATH=..\..\build;%PATH%
set CGO_CFLAGS=-I../../src/api
set CGO_LDFLAGS=-L../../build -lz3

# Run example
go run basic_example.go
```

## API Reference

### Context

- `NewContext()` - Create a new Z3 context
- `NewContextWithConfig(cfg *Config)` - Create context with configuration
- `SetParam(key, value string)` - Set context parameters

### Creating Expressions

- `MkBoolConst(name string)` - Create Boolean variable
- `MkIntConst(name string)` - Create integer variable
- `MkRealConst(name string)` - Create real variable
- `MkInt(value int, sort *Sort)` - Create integer constant
- `MkReal(num, den int)` - Create rational constant

### Boolean Operations

- `MkAnd(exprs ...*Expr)` - Conjunction
- `MkOr(exprs ...*Expr)` - Disjunction
- `MkNot(expr *Expr)` - Negation
- `MkImplies(lhs, rhs *Expr)` - Implication
- `MkIff(lhs, rhs *Expr)` - If-and-only-if
- `MkXor(lhs, rhs *Expr)` - Exclusive or

### Arithmetic Operations

- `MkAdd(exprs ...*Expr)` - Addition
- `MkSub(exprs ...*Expr)` - Subtraction
- `MkMul(exprs ...*Expr)` - Multiplication
- `MkDiv(lhs, rhs *Expr)` - Division
- `MkMod(lhs, rhs *Expr)` - Modulo
- `MkRem(lhs, rhs *Expr)` - Remainder

### Comparison Operations

- `MkEq(lhs, rhs *Expr)` - Equality
- `MkDistinct(exprs ...*Expr)` - Distinct
- `MkLt(lhs, rhs *Expr)` - Less than
- `MkLe(lhs, rhs *Expr)` - Less than or equal
- `MkGt(lhs, rhs *Expr)` - Greater than
- `MkGe(lhs, rhs *Expr)` - Greater than or equal

### Solver Operations

- `NewSolver()` - Create a new solver
- `Assert(constraint *Expr)` - Add constraint
- `Check()` - Check satisfiability (returns Satisfiable, Unsatisfiable, or Unknown)
- `Model()` - Get model (if satisfiable)
- `Push()` - Create backtracking point
- `Pop(n uint)` - Remove backtracking points
- `Reset()` - Remove all assertions

### Model Operations

- `Eval(expr *Expr, modelCompletion bool)` - Evaluate expression in model
- `NumConsts()` - Number of constants in model
- `NumFuncs()` - Number of functions in model
- `String()` - Get string representation

### Bit-vector Operations

- `MkBvSort(sz uint)` - Create bit-vector sort
- `MkBVConst(name string, size uint)` - Create bit-vector variable
- `MkBVAdd/Sub/Mul/UDiv/SDiv(lhs, rhs *Expr)` - Arithmetic operations
- `MkBVAnd/Or/Xor/Not(...)` - Bitwise operations
- `MkBVShl/LShr/AShr(lhs, rhs *Expr)` - Shift operations
- `MkBVULT/SLT/ULE/SLE/UGE/SGE/UGT/SGT(...)` - Comparisons
- `MkConcat(lhs, rhs *Expr)` - Bit-vector concatenation
- `MkExtract(high, low uint, expr *Expr)` - Extract bits
- `MkSignExt/ZeroExt(i uint, expr *Expr)` - Extend bit-vectors

### Floating-Point Operations

- `MkFPSort(ebits, sbits uint)` - Create floating-point sort
- `MkFPSort16/32/64/128()` - Standard IEEE 754 sorts
- `MkFPInf/NaN/Zero(sort *Sort, ...)` - Special values
- `MkFPAdd/Sub/Mul/Div(rm, lhs, rhs *Expr)` - Arithmetic with rounding
- `MkFPNeg/Abs/Sqrt(...)` - Unary operations
- `MkFPLT/GT/LE/GE/Eq(lhs, rhs *Expr)` - Comparisons
- `MkFPIsNaN/IsInf/IsZero(expr *Expr)` - Predicates

### Sequence/String Operations

- `MkStringSort()` - Create string sort
- `MkSeqSort(elemSort *Sort)` - Create sequence sort
- `MkString(value string)` - Create string constant
- `MkSeqConcat(exprs ...*Expr)` - Concatenation
- `MkSeqLength(seq *Expr)` - Length
- `MkSeqPrefix/Suffix/Contains(...)` - Predicates
- `MkSeqAt(seq, index *Expr)` - Element access
- `MkSeqExtract(seq, offset, length *Expr)` - Substring
- `MkStrToInt/IntToStr(...)` - Conversions

### Regular Expression Operations

- `MkReSort(seqSort *Sort)` - Create regex sort
- `MkToRe(seq *Expr)` - Convert string to regex
- `MkInRe(seq, re *Expr)` - String matches regex predicate
- `MkReStar(re *Expr)` - Kleene star (zero or more)
- `MkRePlus(re *Expr)` - Kleene plus (one or more)
- `MkReOption(re *Expr)` - Optional (zero or one)
- `MkRePower(re *Expr, n uint)` - Exactly n repetitions
- `MkReLoop(re *Expr, lo, hi uint)` - Bounded repetition
- `MkReConcat(regexes ...*Expr)` - Concatenation
- `MkReUnion(regexes ...*Expr)` - Alternation (OR)
- `MkReIntersect(regexes ...*Expr)` - Intersection
- `MkReComplement(re *Expr)` - Complement
- `MkReDiff(a, b *Expr)` - Difference
- `MkReEmpty/Full/Allchar(sort *Sort)` - Special regexes
- `MkReRange(lo, hi *Expr)` - Character range
- `MkSeqReplaceRe/ReAll(seq, re, replacement *Expr)` - Regex replace

### Datatype Operations

- `MkConstructor(name, recognizer string, ...)` - Create constructor
- `MkDatatypeSort(name string, constructors []*Constructor)` - Create datatype
- `MkDatatypeSorts(names []string, ...)` - Mutually recursive datatypes
- `MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort)` - Tuples
- `MkEnumSort(name string, enumNames []string)` - Enumerations
- `MkListSort(name string, elemSort *Sort)` - Lists

### Tactic Operations

- `MkTactic(name string)` - Create tactic by name
- `MkGoal(models, unsatCores, proofs bool)` - Create goal
- `Apply(g *Goal)` - Apply tactic to goal
- `AndThen(t2 *Tactic)` - Sequential composition
- `OrElse(t2 *Tactic)` - Try first, fallback to second
- `Repeat(max uint)` - Repeat tactic
- `TacticWhen/Cond(...)` - Conditional tactics

### Probe Operations

- `MkProbe(name string)` - Create probe by name
- `Apply(g *Goal)` - Evaluate probe on goal
- `Lt/Gt/Le/Ge/Eq(p2 *Probe)` - Probe comparisons
- `And/Or/Not(...)` - Probe combinators

### Parameter Operations

- `MkParams()` - Create parameter set
- `SetBool/Uint/Double/Symbol(key string, value ...)` - Set parameters

### Optimize Operations

- `NewOptimize()` - Create optimization context
- `Assert(constraint *Expr)` - Add constraint
- `AssertSoft(constraint *Expr, weight, group string)` - Add soft constraint
- `Maximize(expr *Expr)` - Add maximization objective
- `Minimize(expr *Expr)` - Add minimization objective
- `Check(assumptions ...*Expr)` - Check and optimize
- `Model()` - Get optimal model
- `GetLower/Upper(index uint)` - Get objective bounds
- `Push/Pop()` - Backtracking
- `Assertions/Objectives()` - Get assertions and objectives
- `UnsatCore()` - Get unsat core

### Fixedpoint Operations (Datalog/CHC)

- `NewFixedpoint()` - Create fixedpoint solver
- `RegisterRelation(funcDecl *FuncDecl)` - Register predicate
- `AddRule(rule *Expr, name *Symbol)` - Add Horn clause
- `AddFact(pred *FuncDecl, args []int)` - Add table fact
- `Query(query *Expr)` - Query constraints
- `QueryRelations(relations []*FuncDecl)` - Query relations
- `GetAnswer()` - Get satisfying instance or proof
- `Push/Pop()` - Backtracking

### Quantifier Operations

- `MkQuantifier(isForall bool, weight int, sorts, names, body, patterns)` - Create quantifier
- `MkQuantifierConst(isForall bool, weight int, bound, body, patterns)` - Create with bound vars
- `IsUniversal/IsExistential()` - Check quantifier type
- `GetNumBound()` - Number of bound variables
- `GetBoundName/Sort(idx int)` - Get bound variable info
- `GetBody()` - Get quantifier body
- `GetNumPatterns()` - Number of patterns
- `GetPattern(idx int)` - Get pattern

### Lambda Operations

- `MkLambda(sorts, names, body)` - Create lambda expression
- `MkLambdaConst(bound, body)` - Create lambda with bound variables
- `GetNumBound()` - Number of bound variables
- `GetBoundName/Sort(idx int)` - Get bound variable info
- `GetBody()` - Get lambda body

### Type Variables

- `MkTypeVariable(name *Symbol)` - Create polymorphic type variable sort

### Logging

- `OpenLog(filename string)` - Open interaction log
- `CloseLog()` - Close log
- `AppendLog(s string)` - Append to log
- `IsLogOpen()` - Check if log is open

## Memory Management

The Go bindings use `runtime.SetFinalizer` to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately. The bindings enable `Z3_enable_concurrent_dec_ref` when creating contexts so finalizer-driven decref operations are safe with concurrent GC.

## Thread Safety

Z3 contexts are not thread-safe. Each goroutine should use its own context, or use appropriate synchronization when sharing a context.

## License

Z3 is licensed under the MIT License. See LICENSE.txt in the repository root.

## Contributing

Bug reports and contributions are welcome! Please submit issues and pull requests to the main Z3 repository.

## References

- [Z3 GitHub Repository](https://github.com/Z3Prover/z3)
- [Z3 API Documentation](https://z3prover.github.io/api/html/index.html)
- [Z3 Guide](https://microsoft.github.io/z3guide/)

---

## File: src/api/js/README.md

# TypeScript Bindings

This directory contains JavaScript code to automatically derive TypeScript bindings for the C API, which are published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver).

The readme for the bindings themselves is located in [`PUBLISHED_README.md`](./PUBLISHED_README.md).


## Building

You'll need to have emscripten set up, along with all of its dependencies. The easiest way to do that is with [emsdk](https://github.com/emscripten-core/emsdk). Newer versions of emscripten may break the build; you can find the version used in CI in [this file](https://github.com/Z3Prover/z3/blob/master/.github/workflows/wasm.yml#L13).

Then run `npm i` to install dependencies, `npm run build:ts` to build the TypeScript wrapper, and `npm run build:wasm` to build the wasm artifact.

### Build on your own

Consult the file [build-wasm.ts](https://github.com/Z3Prover/z3/blob/master/src/api/js/scripts/build-wasm.ts) for configurations used for building wasm.

## Tests

Run `npm test` after building to run tests.