Apr 4, 2025
8 mins read
This article is a long time coming. z3, the constraint solver, is commonly used in crackmes and CTF challenges. Wherever possible, I just lift to angr for symbolic execution and bruteforce that way, since z3 is basically math bruteforce anyways.
