angr-in-action/z3example.py

import z3

z = z3.Solver()
x = z3.BitVec('x', 32)
y = z3.BitVec('y', 32)
z.add(x + y == 20)
print(z.check()) # sat -> разрешимо
print(z.model()) # y = 0, x = 20