用途：从反编译伪代码还原出“合法输入必须满足”的比较链或数学等式（如序列号=f(用户名)、flag 逐字节满足某关系），在人工逆推繁琐时交给 Z3 求解器，用于 CTF 逆向/加密题的密钥与 flag 推导。
主要能力：用 BitVec/Int 建模位运算与数学关系，通过 Solver 的 add/check/model 求解 sat/unsat/unknown，支持边界约束、多解枚举与结果提取。
使用方式：安装 pip install z3-solver，验证 python3 -c "import z3; print(z3.get_version_string())"；需 python3 与反编译产物（re-ghidra/re-ida/re-radare2）。步骤为：逐行对照伪代码列出约束清单并转成表达式；按位宽选择 BitVec 或 Int 建模；s.add 后 check，sat 取 model，BitVec 用 as_long() 提取；先加长度/字符集边界再求解；输出后沙箱内喂给原程序验证。
适用场景：无循环、纯确定性等式的约束集合；已展开的逐位 XOR/移位/加减约束；注册机、自定义加密的可逆部分。
限制：长循环逐字节校验应先展开或用 re-angr 符号执行；哈希、非对称验签等不可逆运算无法建模；非线性运算易返回 unknown；需注意位宽不匹配、C 溢出与有符号语义、约束遗漏、PRNG 状态还原可能返回错误模型等问题，求解结果必须交叉验证。