混合执行

沿已走过的路找岔口 ​

随机测试可能长期碰不到 y==x+1。混合执行先用普通输入走一遍，记下“为什么走了这一边”；下一轮有针对性地求一个走另一边的输入。具体运行提供真实控制轨迹，符号条件提供改变输入的方向。

它不需要每次把两条分支的完整程序状态都同时留在内存中，但仍可能探索指数多条路径。减少同时存活状态与消除路径爆炸是不同事情。

从零输入走到断言失败 ​

使用前页返回值程序，输入域先固定为 $D=[-2,2{]}^2$。为了可复算，求解器按字典序选择首个满足输入，调度优先翻转最深未覆盖前缀。

第二轮具体 a=2，符号 a=X+1；二者在 $(1,-2)$ 上一致。第三轮输入不是“把 y 随便加大”，而是求解第二个判断的否定后得到。返回1在原程序上重放也成立，所以它是实际失败输入。

三轮分别到达三条可行路径，最终每个未走过的翻转都已被覆盖或判不可行。这里恰好覆盖全部路径，不能从“通常运行三轮”推广出其他程序的覆盖界。

为什么必须删掉旧后缀 ​

设另一程序先判断 x==0；真分支令 a:=1，假分支令 a:=2；汇合后再次判断 x==0。从 $x=0$ 运行，两个条件都为真。若翻转首判断，却强留第二个旧条件，公式变为 $X\ne 0\wedge X=0$，错误地把有实际运行的目标当成 UNSAT。

正确目标只约束 $X\ne 0$，让新运行自行计算 a=2 并走第二判断的假边。若后续判断还读取分支中被改写的变量，旧后缀也可能带有旧执行的表达式版本；改变前缀后更不能原样沿用。

具体化近似可能漏掉路径 ​

真实工具可能遇到后端不能处理的表达式，便把某个符号量临时换成当前具体值。[1] 这有助于生成测试，但全称覆盖保证随之丢失。例如从 $(X,Y)=(0,0)$ 测试 X*Y==1，若把 $Y$ 固定成0，翻转查询变成 $0\cdot X=1$，得到 UNSAT；实际 $(1,1)$ 却能走真边。

另一些近似会产生满足近似公式、却走不到目标分支的输入，所以新输入重放必须核对前缀。重放失败应记录为模型或搜索偏差，不能登记目标已覆盖。当前下载实现保持精确表达式并枚举有限域，没有这种具体化优化。

找到错误与证明没有错误 ​

一个成功重放的错误输入只依赖那一次运行，证据很短；“没有错误”还要求覆盖全部允许输入路径。超时、只翻最后一个条件、跳过求解失败和截断循环，都可能留下空白。报告应分列已执行测试、已覆盖前缀、不可行目标、unknown 和尚未探索目标。

对并发、时间、随机性或外部服务，重跑同一输入未必重复旧前缀。要么把这些选择纳入输入和记录，要么把保证缩到实际测试轨迹，不能套用确定性证明。

成本按实际运行与查询分别计算 ​

设完成 $r$ 轮运行，第 $i$ 轮执行 ${\ell }_i$ 条语句、遇到 $b_i$ 个判断，则产生至多 $\sum _i{b}_i$ 个翻转尝试，去重后通常更少。总时间包括 $\sum _i{\ell }_i$ 的具体执行、符号表达式处理，以及每个目标的求解与重放；不能仅用“测试次数”表示求解器工作。

使用持久前缀节点时，前缀本体最多按新增分支记录量存储；如果像下载原型那样把每个长度为 $j$ 的前缀都复制成元组，一轮还可能产生 $O(b_i^2)$ 的复制与存储工作。该原型以容易检查为先，不把共享实现的线性前缀成本冒充实际代码成本。

迁移练习：把输入域收紧为 $\{-1,0,1{\}}^2$。仍可走4F和4T、5F，但5T要求 $X>0,Y=X+1$，域中无解；查询应报告该域内 UNSAT。恢复 $[-2,2{]}^2$ 后 $(1,2)$ 又可行，缓存必须失效。这个变化不会证明原来无界整数程序安全。