Using SMT/Z3 to reverse the key checking algorithm.

Original writeup (http://blog.lse.epita.fr/articles/34-hacklu-ctf-2012-donn-beach-500-points.html).