Symex A symbolic executor for Binary Ninja's MLIL. This was used to successfully solve a control flow flattening challenge. Supports SSA form Supports state forking Additional info: Memory is symbolized on load / store Z3 is required