小编Bra*_*rta的帖子

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

我究竟做错了什么？