# Problem

Can you crack the key to decrypt map2 for us? The key to map1 is 11443513758266689915.

## Hint

z3

# Solution

Given the problem and the hint, it is clear that we can use z3 to solve this problem. We can create a z3 `BitVec`

and pass it into the verify function to avoid writing a custom decrypter. Because we don't know the length of the bit vector, I used a conservative estimate of `128`

.