Coffee Hash — Z3 Cyclic Hash Constraint Solving
Model a cyclic windowed hash as a system of linear equations over integer variables and solve it with Z3 to recover the flag.
Constraint-Solving
CrackMat — Z3 Per-Character Quadratic Equations
Each flag character satisfies an independent quadratic equation in integer form; Z3 solves all 20 simultaneously to recover the flag.