Claripy

9.2.209 · active · verified Mon Apr 13

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.

Warnings

breaking The class `claripy.BV` has been renamed to `claripy.BVS` (Bit-Vector Symbol). Old code using `claripy.BV` will break.
Fix: Replace all instances of `claripy.BV` with `claripy.BVS`.
deprecated Accessing bit-vectors via `state.BV` or `state.BVV` within an Angr state is deprecated.
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).
deprecated The `BV.model` attribute is deprecated.
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.
gotcha 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.
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`.

Install

pip install claripy Install stable version

Imports

claripy
```
import claripy
```
Solver
```
import claripy
s = claripy.Solver()
```
Main entry point for creating and managing constraints.
BVS
```
import claripy
x = claripy.BVS('x', 32)
```
claripy.BV was renamed to claripy.BVS (Bit-Vector Symbol) to clarify its purpose.
BVV
```
import claripy
y = claripy.BVV(10, 32)
```
Used to create concrete Bit-Vector Values.

Quickstart

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.

import claripy

s = claripy.Solver()
x = claripy.BVS('x', 8) # Create an 8-bit symbolic bit-vector
y = claripy.BVV(65, 8) # Create an 8-bit concrete bit-vector with value 65

# Add constraints
s.add(claripy.ULT(x, 5)) # Unsigned Less Than x < 5
s.add(x != 1)

# Evaluate the symbolic variable
solutions = s.eval(x, 10) # Get up to 10 possible solutions for x
print(f"Possible values for x: {sorted(solutions)}")
assert sorted(solutions) == [0, 2, 3, 4]

# Max and Min values
print(f"Max value for x: {s.max(x)}")
print(f"Min value for x: {s.min(x)}")

view raw JSON →