Z3

Z3 は、論理式や制約を解くための SMT ソルバーです。

CTF では、フラグ検証条件、数式制約、ビットベクタ演算を解いて入力を求める問題で使われます。