Install & Compatibility
Where this runs
tested against v5.1.0.0 · pip install
no network on importno background threads
Install × environment matrix
Each cell = how many times install + import succeeded across repeated harness runs. Partial = flaky.
glibc = Debian/Ubuntu slim · musl = Alpine Linux
muslpy 3.10–3.95 runs
build_error
glibcpy 3.10–3.95 runs
installs and imports cleanly · install 2.4s · import 0.434s · 68MB
66MB installed
● package 66MB
Code
Verified usage
Verified import paths — ran on the pinned version, not inferred.
*
✓ from z3 import *
This is the most common way to import all Z3 functions and types into the global namespace for convenience.
z3
✓ import z3
✗ Int('x')
When importing as 'import z3', Z3 objects must be prefixed (e.g., 'z3.Int("x")'). Using 'Int("x")' directly will raise a NameError.
This example demonstrates how to create integer variables, add constraints to a solver, check for satisfiability, and retrieve a model if a solution exists.
from z3 import *
# Create integer variables
x = Int('x')
y = Int('y')
# Create a solver instance
s = Solver()
# Add constraints
s.add(x + y == 10)
s.add(x > y)
s.add(y >= 0)
# Check for satisfiability
result = s.check()
if result == sat:
# If satisfiable, print a model
model = s.model()
print(f"Satisfiable! Model: x={model[x]}, y={model[y]}")
elif result == unsat:
print("Unsatisfiable!")
else:
print("Unknown (solver could not determine satisfiability).")
z3 --version
Debug
Known issues
gotchaInteger Division Behavior: When using the division operator `/` with Z3 `Int` types, it performs integer division (Euclidian division) which might not match standard floating-point division or common programming language `//` behavior. This can lead to unexpected results if real number semantics are implicitly assumed. For real division, ensure variables are of `Real` sort or use `ToReal()` for explicit conversion.fixUse `Real('x')` instead of `Int('x')` for real numbers, or explicitly convert using `ToReal(x) / ToReal(y)` if mixed types are needed. affects: All versions where `Int` and `Real` sorts are distinct (fundamental to SMT-LIB and Z3).
gotchaBitVec Signedness Semantics: Operations on `BitVec` (bit-vectors) are interpreted based on signedness (e.g., signed vs. unsigned modulus, shifts) rather than the values themselves. This can differ from typical programming language behavior for operators like `%` and `>>`. Users must explicitly choose signed (`smod`, `sdiv`, `ashr`) or unsigned (`umod`, `udiv`, `lshr`) versions if default Python operators do not align with desired bit-vector semantics.fixFor specific signed/unsigned behavior, use Z3's explicit bit-vector operations like `sdiv`, `udiv`, `srem`, `urem`, `ashr`, `lshr`.
affects: All versions supporting `BitVec` types (fundamental to SMT-LIB and Z3).
gotchaContext and Thread Safety: Z3Py uses a default global context for convenience. However, objects created in different explicit `Context` instances cannot be mixed. It is generally unsafe to access Z3 objects from multiple threads without explicit synchronization, except for the `interrupt()` method which is designed for cross-thread interruption. For multi-threaded applications, create separate `Context` objects per thread.fixAvoid mixing Z3 objects from different `Context` instances. For multi-threading, instantiate a separate `Context` object for each thread to ensure isolation.
affects: All versions (fundamental API design).
gotchaModel for Quantified Variables: When using existential (`Exists`) or universal (`ForAll`) quantifiers, variables declared *within* the quantifier might not appear in the `Solver().model()` output, even if the formula is satisfiable. Only top-level variables declared outside quantifiers are guaranteed to be part of the model.fixTo retrieve values for such variables, restructure the problem to bring them to the top level, or use mechanisms like `model_completion` if your Z3 version and problem structure support it.
affects: All versions (fundamental SMT-LIB model generation).
gotchaNon-Linear Arithmetic Limitations: Z3's performance and completeness can be limited for non-linear arithmetic, especially non-linear *integer* arithmetic. Problems involving exponents (e.g., `2**x`) are generally not handled as polynomials and may result in an `unknown` status. Mixing integers and reals in complex non-linear ways can also lead to hard problems for the solver.fixSimplify or transform non-linear problems into linear forms where possible. For non-linear integer problems, be aware of potential performance/completeness issues. Use `Real` types when non-integer values or continuous functions are intended.
affects: All versions (inherent SMT solver capability).
Upgrade
Version history
5.1.0.0latest on PyPI · released Aug 16, 2026
Audit
Dependencies
PythonrequiredZ3-solver provides Python bindings and requires Python 3.7+ to run.
importlib-resourcesoptionalAutomatically installed for Python versions prior to 3.9 if needed by the package.