我正在使用 z3py 库进行程序验证项目，并且希望对 z3 中的数组访问进行编码。有没有一种简单的方法可以使数组 z3type 具有一定的大小，例如 112 个条目？ 我正在考虑这样的事情: A = Array('A', IntSort(), size)
谢谢
最佳答案
如果你想要一个包含 112 个整数元素的数组，你应该将其声明为
A = IntVector('A', 112)
关于python - z3中一定大小的数组，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/20991530/