私はZ3が初めてで、オンラインのPythonチュートリアルをチェックしていました。Z3でオーバーフローを確認してください
次に、私はBitVecsのオーバーフロー動作をチェックできると思いました。
私はこのコードを書いた：
x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
および値が等しいが、x + 1が0であり、y + 1になるので後継者ではない場合、私は[Y = 7、X = 7（すなわち期待していました8）
しかし、Z3は[y = 0、x = 0]と答える。
私は間違っていますか？
私はあなたが何も悪いことをやっているとは思わないが、BV2Intはバグがあるように見えます：
x = BitVec('x', 3)
prove(x <= 3)
prove(BV2Int(x) <= 3)
Z3pyは最初のものを証明しているが、2番目のための反例x=0を与えます。それは正しいとは言えません。 （奇妙なPythonの問題かもしれませんが、私は方法が分かりません）
また、+がビットベクトルをPythonバインディングの符号付き数値として扱うかどうか、私はそれが事実だと信じています。ただし、BV2Intは、符号なしの値として扱うことはできません。これはさらに問題を複雑にするでしょう。
いずれにしても、BV2Intのように見えます。私はZ3の人々から正式な答えが出るまでそこから離れています。
これが気になる他の人にとって、これはある時点で解決されたようです。このサンプルをz3の最新バージョン（最初の投稿の数年後）で再実行したところ、7,7が返されました。