Warning
Claripy has been rewritten in Rust and is now part of the angr package! The implementation of Claripy found in this repository is now in maintenance mode. This repository is scheduled for archiving on January 1, 2027.
Claripy is an abstracted constraint-solving wrapper.
Project repository: https://github.com/angr/claripy
Documentation: https://api.angr.io/projects/claripy/en/latest/
It is usable!
General usage is similar to Z3:
>>> import claripy
>>> a = claripy.BVV(3, 32)
>>> b = claripy.BVS('var_b', 32)
>>> s = claripy.Solver()
>>> s.add(b > a)
>>> print(s.eval(b, 1)[0])