用 Z3 检查溢出答案

【问题标题】：Check overflow with Z3用 Z3 检查溢出
【发布时间】：2013-07-23 21:20:51
【问题描述】：

我是 Z3 新手，正在查看在线 python 教程。

然后我想我可以检查 BitVecs 中的溢出行为。

我写了这段代码：

x = BitVec('x', 3)
y = Int('y')

solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))

我期待 [y = 7, x = 7]（即当值相等但后继不相等时，因为 x + 1 将是 0 而 y + 1 将是 8）

但是 Z3 的答案是 [y = 0, x = 0]。

我做错了什么？

【问题讨论】：

标签： z3 z3py

【解决方案1】：

我不认为你做错了什么，看起来BV2Int 有问题：

 x = BitVec('x', 3)
 prove(x <= 3)
 prove(BV2Int(x) <= 3)

Z3py 证明了第一个，但给出了第二个反例x=0。这听起来不对。（唯一的解释可能是一些奇怪的 Python 东西，但我不明白如何。）

另请注意，您获得的模型将取决于+ 是否将位向量视为 Python 绑定中的有符号数，我相信是这种情况。但是，BV2Int 可能不会这样做，将其视为无符号值。这会使事情进一步复杂化。

无论如何，看起来BV2Int 不是很干净；在 Z3 人员给出正式答复之前，我会远离它。

【讨论】：

【解决方案2】：

对于其他对此感到担忧的人，这似乎已经在某个时候得到了解决。我刚刚用最新版本的 z3 重新运行了这个示例（在最初发布几年后），它确实返回了 7,7。

【讨论】：