python - Z3py: Array of specific integer type?

Question

In Z3Python, I want to declare an array of bytes (meaning each member of array is of integer of 8 bits). I tried with the following code, but apparently it reports that Int(8) is illegal type.

Any idea on how to fix the problem? Thanks!

I = IntSort()
I8 = Int(8)
A = Array('A', I, I8)

Answer 1

您不能提供数字作为 Int() 函数的参数。它需要一个字符串（实际上是整数的名称），而不是整数的大小（以位为单位）。您可能需要考虑使用位向量：

Byte = BitVecSort(8)
i8 = BitVec('i8', Byte)
A = Array('A', IntSort(), Byte)