Tags: rev z3 

Rating: 5.0

Solving the challenge using the Python module Z3 Solver.

Original writeup (https://gist.github.com/Leoid/27f814bb8bd6105bab9e842c8f96d28c).