{"id":3326,"library":"z3-solver","title":"Z3 Solver","description":"Z3 is a high-performance theorem prover developed by Microsoft Research, primarily used for Satisfiability Modulo Theories (SMT) problems. It supports various data types including bitvectors, booleans, arrays, floating point numbers, and strings, making it a versatile tool for formal verification, software/hardware testing, and constraint solving. The library is actively maintained with frequent minor releases and is currently on version 4.16.0.0.","status":"active","version":"4.16.0.0","language":"en","source_language":"en","source_url":"https://github.com/Z3Prover/z3","tags":["smt","solver","verification","logic","constraint-solving","formal-methods"],"install":[{"cmd":"pip install z3-solver","lang":"bash","label":"Install Z3 Solver"}],"dependencies":[{"reason":"Z3-solver provides Python bindings and requires Python 3.7+ to run.","package":"Python","optional":false},{"reason":"Automatically installed for Python versions prior to 3.9 if needed by the package.","package":"importlib-resources","optional":true}],"imports":[{"note":"This is the most common way to import all Z3 functions and types into the global namespace for convenience.","symbol":"*","correct":"from z3 import *"},{"note":"When importing as 'import z3', Z3 objects must be prefixed (e.g., 'z3.Int(\"x\")'). Using 'Int(\"x\")' directly will raise a NameError.","wrong":"Int('x')","symbol":"z3","correct":"import z3"}],"quickstart":{"code":"from z3 import *\n\n# Create integer variables\nx = Int('x')\ny = Int('y')\n\n# Create a solver instance\ns = Solver()\n\n# Add constraints\ns.add(x + y == 10)\ns.add(x > y)\ns.add(y >= 0)\n\n# Check for satisfiability\nresult = s.check()\n\nif result == sat:\n    # If satisfiable, print a model\n    model = s.model()\n    print(f\"Satisfiable! Model: x={model[x]}, y={model[y]}\")\nelif result == unsat:\n    print(\"Unsatisfiable!\")\nelse:\n    print(\"Unknown (solver could not determine satisfiability).\")","lang":"python","description":"This example demonstrates how to create integer variables, add constraints to a solver, check for satisfiability, and retrieve a model if a solution exists."},"warnings":[{"fix":"Use `Real('x')` instead of `Int('x')` for real numbers, or explicitly convert using `ToReal(x) / ToReal(y)` if mixed types are needed.","message":"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.","severity":"gotcha","affected_versions":"All versions where `Int` and `Real` sorts are distinct (fundamental to SMT-LIB and Z3)."},{"fix":"For specific signed/unsigned behavior, use Z3's explicit bit-vector operations like `sdiv`, `udiv`, `srem`, `urem`, `ashr`, `lshr`.","message":"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.","severity":"gotcha","affected_versions":"All versions supporting `BitVec` types (fundamental to SMT-LIB and Z3)."},{"fix":"Avoid mixing Z3 objects from different `Context` instances. For multi-threading, instantiate a separate `Context` object for each thread to ensure isolation.","message":"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.","severity":"gotcha","affected_versions":"All versions (fundamental API design)."},{"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.","message":"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.","severity":"gotcha","affected_versions":"All versions (fundamental SMT-LIB model generation)."},{"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.","message":"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.","severity":"gotcha","affected_versions":"All versions (inherent SMT solver capability)."}],"env_vars":null,"last_verified":"2026-04-11T00:00:00.000Z","next_check":"2026-07-10T00:00:00.000Z"}