python - Bit Vector 戦術により、Z3Py で終了コード 139 が発生する

Question

これは単純なビット ベクトルの問題です。

import z3

s = z3.Tactic('bv').solver()
m = z3.Function('m', z3.BitVecSort(32), z3.BitVecSort(32))
a, b = z3.BitVecs('a b', 32)

axioms = [
    a == m(12432),
    z3.Not(a == b)
]

s.add(axioms)
print(s.check())

Python がエラー コード 139 でクラッシュします。注意してください、これは私の本当の問題ではないので、私のプロジェクトではビット ベクトル タクティクスを使用する必要がありsmtますが、タクティックまたはタクティックに問題はありませんqfbv。