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.
