Using GDB to unpack, Binary Ninja to analyse, and finally Z3 to solve the translated binary code in Python.

Original writeup (https://fascinating-confusion.io/posts/2020/04/reee-writeup/).