1  #!/usr/bin/env python
 2  
 3  from claripy import BVS, BVV, Solver, Or, RotateLeft, RotateRight, And
 4  
 5  s=Solver(timeout=1728000000, max_memory=110 * 1024**3)
 6  
 7  tgt = BVS('tgt', 8, explicit_name='tgt')
 8  dep = tgt ^ (tgt << 1)
 9  sol = s.eval(tgt, 10, extra_constraints=[dep==11])
10  print([f"{x:02x}" for x in sol])