我目前正在研究将通过C程序的“路径”转换为相应的SMT查询以测试该路径的可行性的代码。我有创建SMT-LIB v1.2查询的工作代码，该代码使用Z3 2.11和QF_AUFBV逻辑来解决查询。我目前正在将此代码移植到Z3 4.3，以利用此后可能发生的任何速度提升，尤其是因为我以前的代码似乎花很长时间（大约22分钟）处理仅向其分配24个值的查询一个三维数组，并检查数组中某个位置的值。
但是，似乎QF_AUFBV逻辑（从SMT-LIB v2.0标准开始）不再支持多维数组，或者不再支持其值也是数组的数组（可能更深）。一旦从查询中删除“（set-logic QF_AUFBV）”行，Z3 4.3就可以处理该查询，但是仍然需要很长时间。
我想知道是否有人知道为什么在SMT-LIB v2.0标准中停止了对多维数组的支持，以及我可以使用哪些替代逻辑。我还想知道，当我删除指定QF_AUFBV理论的那一行时，Z3到底在使用什么逻辑。
谢谢！
SMT-LIB标准从不支持多维数组。Z3可以处理它们，但它们不是标准的一部分。SMT-LIB 1.0是一种限制性很强的格式，因此Z3进行了多种扩展来满足用户需求。另一方面，SMT-LIB 2.0是一种非常丰富的输入格式，可解决用户使用SMT-LIB 1.0时遇到的主要问题。在Z3 4.x中，当在输入文件中指定逻辑时，Z3尝试符合SMT-LIB 2.0标准。当set-logic被删除，所有Z3特定扩展名被启用。
如您所述，数组sorrt (Array I1 I2 R)可以编码为(Array I1 (Array I2 R))。
关于性能，Z3 3.x和4.x在阵列理论上没有性能改进。它们对位向量有很多改进，但是当问题将数组和位向量混合在一起时，它们将不可用。一种新的阵列理论已经出现在TODO列表中，但Z3团队目前尚无人在研究。