我是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]。
我做错了什么?
我不认为你做错了什么,看起来 BV2Int
有bug:
x = BitVec('x', 3)
prove(x <= 3)
prove(BV2Int(x) <= 3)
x=0
。这听起来不太对。(唯一的解释可能是一些奇怪的Python问题,但我不知道是哪种情况。)此外,请注意所得到的模型将取决于在Python绑定中+
是否将位向量作为带符号数字处理,我认为是这种情况。然而,BV2Int
可能不这样做,将其视为无符号值。这会进一步复杂化事情。无论如何,看起来BV2Int
不是很可靠,直到Z3团队有正式答案之前,最好避免使用它。对于其他关注此事的人,这个问题似乎已经在某个时候得到了解决。我刚刚使用最新版本的z3重新运行了这个示例(在最初发布几年后),它确实返回了7,7。