BitVecs が z3 でどのように機能するかを理解していないと思います。私は次のコードを書きました：
>>> import z3
>>> s = z3.Solver()
>>> a = z3.BitVec("a", 32)
>>> s.add(z3.ForAll(a, z3.Not(z3.And(a > 2147483647, a < 2147484671))))
この範囲の内外に値があるため、これは「unsat」であると予想されます。しかし、実行するs.check()と、次のようになります。
>>> s.check()
sat
これは私を混乱させたので、オーバーフローが関係していると推測しました。しかし、私は試しました：
>>> b = z3.BitVec("b", 32)
>>> s = z3.Solver()
>>> s.add(b == 2147484671)
>>> s.check()
sat
>>> s.model()
[b = 2147484671]
z3 が 32 ビット BitVecs を使用してこの数値をモデル化できることを示唆しているため、これは私を大いに混乱させます。さらに私は走った：
>>> s = z3.Solver()
>>> c = z3.BitVec("c", 32)
>>> s.add(z3.And(c > 2147483647, c < 2147484671))
>>> s.check()
unsat
2番目の例とは明らかに互換性がないように見えるため、さらに混乱しました...