z3中一定大小的数组

【问题标题】：An array of a certain size in z3z3中一定大小的数组
【发布时间】：2014-01-08 09:25:40
【问题描述】：

我正在将 z3py 库用于程序验证项目，并希望对 z3 中数组的访问进行编码。有没有一种简单的方法可以使 Array z3type 具有一定的大小，例如 112 个条目？我在想类似的东西：A = Array('A', IntSort(), size)

谢谢，

【问题讨论】：

【解决方案1】：

如果你想要一个包含 112 个整数元素的数组，你应该将它声明为

A = IntVector('A', 112)

【讨论】：