Applied a black box approach to solve the challenge. Used the Z3 Thorem prover.

https://0xec.blogspot.com/2017/11/tuctf-write-up-re-track_18.html

Original writeup (https://0xec.blogspot.com/2017/11/tuctf-write-up-re-track_18.html).