"Z3中特定大小的数组"

Question

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

谢谢

Answer 1

如果需要一个包含112个整数元素的数组，则应将其声明为

A = IntVector('A', 112)