Tags: z3
Rating:
TL;DR. Parse the checking functions to extract the constraints and solve for the flag. Or use ANGR. I don't know how to use ANGR so it's the old-fashioned way for me: walking through the binary with a clunky FSA and solving with Z3.