{"id":5150,"library":"claripy","title":"Claripy","description":"Claripy is an abstraction layer for constraint solvers, providing a unified way to interact with concrete and symbolic expressions. It acts as the solver engine for the Angr binary analysis framework. The library allows users to define symbolic variables, add constraints, and evaluate expressions using various backends like Z3. The current version is 9.2.209, with releases closely tied to the Angr project's development cycle, most recently updated on April 7, 2026.","status":"active","version":"9.2.209","language":"python","source_language":"en","source_url":"https://github.com/angr/claripy","tags":["constraint solver","symbolic execution","SMT","bitvector","angr","binary analysis"],"install":[{"cmd":"pip install claripy","lang":"bash","label":"Install stable version"}],"dependencies":[{"reason":"Used for caching mechanisms within the solver engine.","package":"cachetools","optional":false},{"reason":"Provides backported and future typing features.","package":"typing-extensions","optional":false},{"reason":"Primary SMT solver backend for symbolic execution. Requires a specific version (e.g., 4.13.0.0) for full compatibility.","package":"z3-solver","optional":false}],"imports":[{"symbol":"claripy","correct":"import claripy"},{"note":"Main entry point for creating and managing constraints.","symbol":"Solver","correct":"import claripy\ns = claripy.Solver()"},{"note":"claripy.BV was renamed to claripy.BVS (Bit-Vector Symbol) to clarify its purpose.","wrong":"x = claripy.BV('x', 32)","symbol":"BVS","correct":"import claripy\nx = claripy.BVS('x', 32)"},{"note":"Used to create concrete Bit-Vector Values.","symbol":"BVV","correct":"import claripy\ny = claripy.BVV(10, 32)"}],"quickstart":{"code":"import claripy\n\ns = claripy.Solver()\nx = claripy.BVS('x', 8) # Create an 8-bit symbolic bit-vector\ny = claripy.BVV(65, 8) # Create an 8-bit concrete bit-vector with value 65\n\n# Add constraints\ns.add(claripy.ULT(x, 5)) # Unsigned Less Than x < 5\ns.add(x != 1)\n\n# Evaluate the symbolic variable\nsolutions = s.eval(x, 10) # Get up to 10 possible solutions for x\nprint(f\"Possible values for x: {sorted(solutions)}\")\nassert sorted(solutions) == [0, 2, 3, 4]\n\n# Max and Min values\nprint(f\"Max value for x: {s.max(x)}\")\nprint(f\"Min value for x: {s.min(x)}\")","lang":"python","description":"This quickstart demonstrates how to initialize a Claripy solver, create symbolic and concrete bit-vectors, add constraints, and then evaluate the possible values for the symbolic variable. It showcases basic operations like `BVS` for symbolic variables, `BVV` for concrete values, `add` for constraints, and `eval`, `max`, `min` for solution retrieval."},"warnings":[{"fix":"Replace all instances of `claripy.BV` with `claripy.BVS`.","message":"The class `claripy.BV` has been renamed to `claripy.BVS` (Bit-Vector Symbol). Old code using `claripy.BV` will break.","severity":"breaking","affected_versions":"Likely around Angr 4.6.3.28 release cycle (older versions)"},{"fix":"Use `state.se.BVS` and `state.se.BVV` instead when working with symbolic expressions attached to an Angr state (`state.se` refers to the symbolic execution engine).","message":"Accessing bit-vectors via `state.BV` or `state.BVV` within an Angr state is deprecated.","severity":"deprecated","affected_versions":"Likely around Angr 4.6.3.28 release cycle (older versions)"},{"fix":"Instead of `BV.model`, convert the bit-vector with the appropriate backend directly, e.g., `claripy.backend_concrete.convert(bv)` if you need a specific model.","message":"The `BV.model` attribute is deprecated.","severity":"deprecated","affected_versions":"Likely around Angr 4.6.3.28 release cycle (older versions)"},{"fix":"Ensure `z3-solver` is installed at the exact version specified by Claripy's `pyproject.toml` or the Angr project. For current versions, this is `z3-solver==4.13.0.0`.","message":"Claripy has strong dependencies on specific `z3-solver` versions. Incompatibilities can lead to `AttributeError` (e.g., `Z3_get_symbol_string_bytes`) or functional issues, especially with floating-point operations.","severity":"gotcha","affected_versions":"All versions, especially when upgrading `z3-solver` independently."}],"env_vars":null,"search_vec":"'2026':73 '7':72 '9.2.209':55 'abstract':5 'act':22 'add':41 'allow':35 'analysi':31,82 'angr':29,62,80 'april':71 'backend':48 'binari':30,81 'bitvector':79 'claripi':1,2 'close':58 'concret':17 'constraint':8,42,74 'current':52 'cycl':66 'defin':38 'develop':65 'engin':26 'evalu':44 'execut':77 'express':20,45 'framework':32 'interact':15 'layer':6 'librari':34 'like':49 'project':63 'provid':10 'recent':68 'releas':57 'smt':78 'solver':9,25,75 'symbol':19,39,76 'tie':59 'unifi':12 'updat':69 'use':46 'user':36 'variabl':40 'various':47 'version':53 'way':13 'z3':50","created_at":"2026-04-14T01:21:21.482056+00:00","updated_at":"2026-04-17T14:48:43.799241+00:00","problems":[{"fix":"Review the constraints being added to the solver, especially those involving logical operations (AND, OR) or comparisons, to identify and remove conflicting conditions. Use `solver. satisfiable()` to check for satisfiability before attempting to evaluate, and `solver.unsat_core` if available, to identify the subset of constraints causing unsatisfiability.","cause":"The set of constraints added to the Claripy solver are contradictory, meaning there are no possible values for the symbolic variables that can satisfy all conditions simultaneously.","error":"claripy.errors.UnsatError"},{"fix":"Ensure that all BitVector objects involved in an operation (e.g., concatenation, arithmetic, comparisons) have compatible bit widths. Use methods like `extend()`, `zero_extend()`, `sign_extend()`, or `Extract()` to adjust bit widths as necessary before performing the operation.","cause":"This error occurs when attempting to perform an operation on Claripy BitVector (BV) or BitVectorValue (BVV) objects that have different or incompatible bit widths, and the operation requires them to be of the same size.","error":"ClaripySizeError: bitwidth mismatch"},{"fix":"Distinguish between concrete Python integers and Claripy symbolic BitVector objects. When working with symbolic variables, ensure they are created using `claripy.BVS()` or `claripy.BVV()` and operations are performed using Claripy's methods. Convert concrete values to Claripy BVVs if they need to interact with symbolic expressions, e.g., `claripy.BVV(10, 32)`.","cause":"This error arises when a standard Python integer is treated as a Claripy symbolic object, specifically when trying to access attributes or methods (like `symbolic`) that only exist on Claripy AST objects.","error":"AttributeError: 'int' object has no attribute 'symbolic'"},{"fix":"Claripy AST objects represent expressions, not functions. Instead of calling the AST object directly, use Claripy's solver methods (e.g., `solver.eval()`, `solver.min()`, `solver.max()`) to evaluate the expression to concrete values, or use appropriate AST methods for manipulation (e.g., `.zero_extend()`, `.chop()`). Remember that operations like `a + b` construct new ASTs, they don't 'call' `a` or `b`.","cause":"This error typically occurs when a Claripy Abstract Syntax Tree (AST) object, particularly a base AST or a specific type like a BitVector, is incorrectly treated as a function and an attempt is made to call it.","error":"TypeError: 'claripy.ast.Base.Base' object is not callable"},{"fix":"First, ensure your `z3-solver` and `claripy` installations are up-to-date, as this often resolves compatibility issues. If the problem persists, try to isolate the specific Claripy operation or set of constraints that trigger the error to report a more detailed bug to the Claripy/Angr project. Sometimes, simplifying complex expressions or constraints can help Z3 process them more reliably.","cause":"This indicates an underlying issue within the Z3 SMT solver backend that Claripy uses. It can be caused by an outdated Z3 version, an unexpected input format passed to Z3, or an internal Z3 bug that Claripy's abstraction layer cannot handle.","error":"BackendError: Unknown Z3 error in abstraction"}],"ecosystem":"pypi","meta_description":null,"install_score":null,"quickstart_score":null,"quickstart_tag":null,"pypi_latest":"9.3.3","cli_name":"","cli_version":null,"type":"library","homepage":null,"github":"https://github.com/angr/claripy","docs":null,"changelog":null,"pypi":"https://pypi.org/project/claripy/","npm":null,"openapi_spec":null,"status_page":null,"smithery":null,"categories":["ai-ml","http-networking","data"],"base_url":null,"auth_type":null,"provenance":{"verified_status":"passing","verified_at":"2026-06-28","last_verified":"2026-08-30","next_check":"2026-07-28","install_tag":null}}