python - (Z3Py) 連結、量指定子、およびビットベクトル

Question

ビットベクトルと連結で量指定子を利用することは可能ですか? 説明のために、最新の Z3 で次のコードを実行します。

a = BitVec('a', 8)
b = Concat(BitVec('b', 4), BitVec('c', 4))

prove(ForAll(a, Exists(b, a == b)))

次のエラーが発生します。

BitVecRef instance has no attribute '__len__'

簡単な__len__メソッドを追加しようとしましBitVecRefたが、さらに問題が発生しました。

がなくてもConcat、コードは期待どおりに機能します。例えば：

a = BitVec('a', 8)
b = BitVec('b', 8)

prove(ForAll(a, Exists(b, a == b)))

正しい出力：proved