符号执行

把输入当符号而非具体值执行，走到每个分支时收集路径条件，再用求解器找触发输入。