6

我是 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]。

我究竟做错了什么?

4

2 回答 2

5

我认为您没有做错任何事情,看起来像 BV2Int错误:

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

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

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

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

于 2013-07-24T01:46:36.140 回答
2

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

于 2017-12-04T06:04:52.223 回答