Tags: python z3 reverse 

Rating:

Solve it using Z3 SAT solver

Original writeup (https://github.com/Hong5489/TJCTF2020/tree/master/comprehensive2).