python - (Z3Py)Concat，量词和位向量

是否可以使用带位向量和串联的量词？为了说明这一点，请在最新的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

最佳答案

您的示例将值b定义为串联的简写。
它作为绑定变量传递到量词Exists（b，a == b）。
量词需要一个基本常量列表，例如下面的a，b，c，但不包含复合常量
表达式，例如d。以下是您处理过的难题的一个版本：

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

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