opt: manage temporary search scopes with guards (#10896)

Summary

Replace manual push/pop counters in optsmt::geometric_opt and geometric_lex with a small local guard that removes the temporary scopes it tracks.
Use the existing solver::scoped_push in bisect, removing repeated cleanup in its SAT, UNSAT, and UNKNOWN paths.
Keep normal pop timing, including before nlsat/bisection fallback and before publishing bisection models. Search decisions, bound handling, callbacks, and resource budgets are unchanged on normal paths.
Remove leftover trial bounds on cancellation and exceptions. No new order interface or optimization driver is introduced.

Regression coverage

Add six deterministic cases to opt_bounds: force UNKNOWN, cancellation, or an exception during either a geometric trial or the first bisection trial.

The problem is to maximize real x with x >= 0 and x*x <= 2. Exact nlsat optimization is disabled so the tests exercise the rational-bound fallback. Each case checks that the earlier scope and original assertions remain, x = 0 is still feasible after cleanup, and the same optimizer and solver can be used again.

Validation

Build z3 and test-z3 in Release and Debug; run opt_value, opt_bounds, opt_nlsat, and opt_pareto in both.
Run all 83 selected optimization regressions from the local z3test checkout against the parent Release binary and the changed Release and Debug binaries. All pass, with byte-for-byte identical output.
Link the new regression suite against the original optsmt.cpp: it fails the scope-balance assertion after an exception. The changed implementation passes.
Pass Python solver/model and repeated Optimize push/pop checks, the CLI smoke check, and all four benchmark controls.
git diff --check passes.

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com Copilot-Session: 7f015642-9f30-4d9a-ae34-55311f2b64e7

Z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. Windows binary distributions include C++ runtime redistributables

If you are not familiar with Z3, you can start here.

Pre-built binaries for stable and nightly releases are available here.

Z3 can be built using CMake, vcpkg, or Bazel. It provides bindings for several programming languages.

See the release notes for notes on various stable releases of Z3.

Build status

Pull Request & Push Workflows

WASM Build	Windows Build	CI	OCaml Binding

Scheduled Workflows

Android Build	Pyodide Wheel (PyPI)	Nightly Build	Cross Build	F* Master Build

MSVC Static	MSVC Clang-CL	Build Z3 Cache	Memory Safety	Mark PRs Ready

Manual & Release Workflows

Documentation	Release Build	WASM Release

Specialized Workflows

Nightly Validation	Copilot Setup	Agentics Maintenance

Agentic Workflows

API Coherence	Code Simplifier	Release Notes	Workflow Suggestion	Academic Citation

Issue Backlog	Memory Safety Report	SMTLIB Benchmark Finder

Building Z3 using CMake

CMake is the preferred and most fully featured build system for Z3. A basic release build is:

cmake -S . -B build -DCMAKE_BUILD_TYPE=Release
cmake --build build --parallel $(nproc)

See README-CMake.md for build options, language bindings, installation, and instructions for consuming Z3 from another CMake project.

Z3 uses C++20. On Windows, the recommended version of Visual Studio is therefore VS2019 or later; CMake with the Ninja or Visual Studio generator builds Z3 from the Visual Studio Command Prompt.

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 cmake -S . -B build -DZ3_ENABLE_CFG=OFF if needed

Use sudo cmake --install build to install to the system prefix (or set -DCMAKE_INSTALL_PREFIX= at configure time for a custom prefix). To uninstall, consult your platform’s package manager, or, since CMake tracks installed files in build/install_manifest.txt, remove those files directly.

Building Z3 using vcpkg

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

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

With CMake, use the -DZ3_BUILD_DOTNET_BINDINGS=ON option.

See examples/dotnet for examples.

`C`

These are always enabled.

See examples/c for examples.

`C++`

These are always enabled.

See examples/c++ for examples.

`Java`

With CMake, use the -DZ3_BUILD_JAVA_BINDINGS=ON option.

For IDE setup instructions (Eclipse, IntelliJ IDEA, Visual Studio Code) and troubleshooting, see the Java IDE Setup Guide.

See examples/java for examples.

`Go`

With CMake, use the -DZ3_BUILD_GO_BINDINGS=ON option. Note that Go bindings use CGO and require a Go toolchain (Go 1.20 or later) to build.

See examples/go for examples and src/api/go/README.md for complete API documentation.

`OCaml`

With CMake, use the -DZ3_BUILD_OCAML_BINDINGS=ON option.

See examples/ml for examples.

`Python`

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

   pip install z3-solver

With CMake, use the -DZ3_BUILD_PYTHON_BINDINGS=ON option.

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 -DCMAKE_INSTALL_PYTHON_PKG_DIR= option to change the Python package directory used for installation. For example:

cmake -S . -B build -DCMAKE_INSTALL_PREFIX=/home/leo -DZ3_BUILD_PYTHON_BINDINGS=ON -DCMAKE_INSTALL_PYTHON_PKG_DIR=/home/leo/lib/python3.x/site-packages

If you do need to install to a non-standard prefix, a better approach is to use a Python virtual environment and install Z3 there. 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.

virtualenv venv
source venv/bin/activate
cmake -S . -B build -DCMAKE_INSTALL_PREFIX=$VIRTUAL_ENV -DZ3_BUILD_PYTHON_BINDINGS=ON
cmake --build build --parallel $(nproc)
cmake --install build
# 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 for examples.

`Julia`

The Julia package 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.

`WebAssembly` / `TypeScript` / `JavaScript`

A WebAssembly build with associated TypeScript typings is published on npm as z3-solver. Information about building these bindings can be found in src/api/js.

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

Project MachineArithmetic provides a Smalltalk interface to Z3’s C API. For more information, see MachineArithmetic/README.md.

AIX

Build settings for AIX are described here.

System Overview

System Diagram

Interfaces

Default input format is SMTLIB2
Other native foreign function interfaces:
C++ API
.NET API
Java API
Python API (also available in pydoc format)
Rust
C
OCaml
Julia
Smalltalk (supports Pharo and Smalltalk/X)

Power Tools

The Axiom Profiler currently developed by ETH Zurich

Policy for filing fuzz bugs

Z3 is a popular target for fuzzers. Many (best) papers have been published on finding bugs in z3 and SMT solvers and without doubt the bug file/fix ratio plays an important role establishing evidence in the publications for the value of fuzz tools. Unfortunately, addressing fuzz bugs doesn’t necessarily advance uses of z3 where it matters most to users, and efforts to address them takes time away from such activities. With rapidly increasing quality of coding agents for diagnostics and fixes it is now a reasonable ask that fuzz bug reports make a solid effort on diagnostics and fix. To help focus efforts on what matters, fuzz bugs without further analysis than a repro may be closed without further consideration.