This challenge give a source code.
5 x 5 matrix set -> using z3 to solve this challenge

Original writeup (https://github.com/vngkv123/CTF/blob/master/ctf_in_2017/tuctf/future.py).