我是 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]。
我究竟做错了什么?