使用Z3证明二分查找终止性时遭遇无效反例的问题

问题背景 #

我正在学习使用Z3工具证明二分查找的终止性，核心思路是证明循环中无论执行哪个分支，规模函数(r - l)始终递减。注意：我假设查找范围是左闭右开区间。

初始代码如下：

from z3 import *

# 证明二分查找必然终止
# 核心依据是无论循环走哪个分支，r - l的取值始终递减

l, r = Ints("l r")

preconditions = And([
    l >= 0,
    r > l, # 假设查找范围非空
])

mid = Int("mid")
termination = And([
    mid == (l + r) / 2,
    (r - l) > (mid - l),
    (r - l) > (r - mid + 1),
])

claim = Implies(preconditions, termination)

prove(claim)

异常现象 #

执行上述代码后，Z3返回了一个反例：

counterexample
[l = 0, mid = 1, r = 1]

这个结果让我困惑，因为终止条件里明确要求mid == (l + r) / 2，而当l=0、r=1时，整数除法(0+1)/2的结果是0，不可能等于1。

为了排除变量mid的影响，我将mid直接内联到终止条件中，修改后的代码片段：

termination = And([
    (r - l) > ((l + r) / 2 - l),
    (r - l) > (r - (l + r) / 2 + 1),
])

但运行后仍然得到反例：

counterexample
[l = 0, r = 1]

验证过程 #

1. 确认Z3的整数除法行为：

>>> from z3 import *
>>> x, y = Ints("x y")
>>> ((x + y) / 2).sort()
Int

结果证明Z3确实是按整数类型处理除法，没有转换为实数。

2. 验证反例的合法性：

solve(mid == 1, mid == (l + r) / 2, l == 0, r == 1)

Z3返回无解，说明该反例根本不满足mid的定义。

疑问 #

为什么Z3会判定这些明显不符合约束的反例有效？我原本期望Z3能证明我的断言成立。

内容的提问来源于stack exchange，提问作者Youssef Ibrahim