用Z3检查溢出

Question

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

我究竟做错了什么？

Answer 1

我不认为你做错了什么,看起来像 BV2Int马车:

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

Z3py证明了第一个,但给出x=0了第二个例子.这听起来不对.(唯一的解释可能是一些奇怪的Python事情,但我不知道如何.)

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

在任何情况下,看起来BV2Int都不是犹太人; 我会远离它,直到有Z3人的官方回答.