Z3 Solver

Warnings

• gotcha Integer 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.
  Fix: Use `Real('x')` instead of `Int('x')` for real numbers, or explicitly convert using `ToReal(x) / ToReal(y)` if mixed types are needed.
• gotcha BitVec 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.
  Fix: For specific signed/unsigned behavior, use Z3's explicit bit-vector operations like `sdiv`, `udiv`, `srem`, `urem`, `ashr`, `lshr`.
• gotcha Context 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.
  Fix: Avoid mixing Z3 objects from different `Context` instances. For multi-threading, instantiate a separate `Context` object for each thread to ensure isolation.
• gotcha Model 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.
  Fix: To 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.
• gotcha Non-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.
  Fix: Simplify 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.

Install

• pip install z3-solver Install Z3 Solver

Imports

• *

  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

  When importing as 'import z3', Z3 objects must be prefixed (e.g., 'z3.Int("x")'). Using 'Int("x")' directly will raise a NameError.

Quickstart

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