我正在研究验证机器代码程序。由于许多现代 SMT 求解器有效地支持数组，我计划在我们的验证工具中使用它们。我正在玩 z3，我注意到对公式的微小更改会导致超时。
以下是我使用的两个示例：
1) http://rise4fun.com/Z3/e4Ci *公式：= (array_32_8_0_1_0 == array_32_8_0_0_0) And (EBP_1_1_0 == EBP_1_0_0) And (Not(array_32_8_0_1_0[EBP_1_1_0 - 0] == array_32_8_0_1_0[EBP_1_0_0])) * 对于这个例子，我感到不安，这很好！
2) http://rise4fun.com/Z3/t8aT *公式：= (array_32_8_0_1_0 == array_32_8_0_0_0) 和 (EBP_1_1_0 == EBP_1_0_0) 和 (Not(array_32_8_0_1_0[EBP_1_1_0 - 1] == array_32_8_0_1_0[EBP_1_0_0])) * 对于这个例子，我得到了一个超时。在我的机器上用 z3.exe 运行一个小时也没有给我任何东西。此示例与 (1) 几乎相同，只是数组访问涉及线性表达式。（看第 16 行 temp-var-4 的定义）
为什么会这样？它是否与位向量和数组理论的结合有关？