在Z3Python中，我想声明一个字节数组(意味着数组的每个成员都是8位整数)。我尝试使用以下代码，但显然它报告 Int(8) 是非法类型。
知道如何解决这个问题吗？谢谢!
I = IntSort()
I8 = Int(8)
A = Array('A', I, I8)
最佳答案
您不能提供数字作为 Int() 函数的参数。它需要一个字符串(实际上是整数的名称)，而不是整数的大小(以位为单位)。您可能需要考虑使用位向量:
Byte = BitVecSort(8)
i8 = BitVec('i8', Byte)
A = Array('A', IntSort(), Byte)
关于python - Z3py : Array of specific integer type?，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/15331203/