定义结构体字段访问的逻辑函数后，Why WP结合Z3为何能证明显式为\false的ACSL契约？

嗨，这个问题确实挺反直觉的，我来帮你拆解一下背后的原因：

首先咱们先明确你的场景：你写了两个C函数f和g，它们的ACSL契约里都有ensures \false——这是一个明显不可能成立的结论，正常来说只要函数能被合法调用（比如f里满足g的前置条件后调用它），验证器应该无法证明这个契约才对。但你加入了一个看似没用的逻辑函数getN后，Z3居然把所有9个目标都证明了，而Alt-Ergo和CVC4却做不到，这本质上是Z3处理Frama-C WP生成的一阶逻辑目标时的特殊行为导致的。

关键原因：逻辑函数getN带来的逻辑转换偏差 #

你定义的getN逻辑函数：

/*@ axiomatic Block {
  predicate isZero(int left) =
  left == 0;
  // Unused, but necessary for verification
  logic int getN(struct S *s) = s->n;
}*/

虽然它在代码里没被直接调用，但Frama-C的WP插件会把这个逻辑函数转换成一阶逻辑中的等价定义，也就是getN(s) ≡ s->n。当WP为g函数生成验证目标时，目标是：

假设\valid(s)且isZero(s->n)（即s->n == 0），证明\false

正常来说这个目标是不可证的，因为前提是可满足的（比如f函数里的调用就满足所有前置条件），不可能从真前提推导出假结论。但Z3在处理这个等价定义时，出现了特殊的行为：

• Z3的量词处理和模型构造逻辑，可能错误地将这个等价关系判定为某种隐含矛盾，或者在构造满足前提的模型时失败，从而空洞地认为前提不可满足——在一阶逻辑里，如果前提不可满足，那么任何结论（包括\false）都会被视为成立。

为什么其他Prover不会出现这个问题？ #

Alt-Ergo和CVC4对这类逻辑定义的处理更严谨，它们能正确识别到\valid(s)且s->n ==0是可满足的（存在对应的模型，比如f里的局部变量s），所以无法推导出\false这个结论，这才是符合预期的验证结果。

你可以尝试的解决/验证方式 #

• 移除冗余的逻辑函数：删掉那个没用的getN，再用Z3验证，应该就会得到正确的“无法证明”结果
• 交叉验证：用Alt-Ergo或CVC4作为Prover来验证，它们的结果更符合预期
• 更新Z3版本：这个问题可能是Z3 4.12.2的特定bug，尝试更新到更高版本的Z3，看看是否已经修复

备注：内容来源于stack exchange，提问作者ReMarxist