我想知道，如果我能让 Z3“记住”数组的更新。
例如，以下输入是可满足的：
(declare-const x Int)
(declare-const a1 (Array Int Int))
(assert (= (select (store a1 x 2) x) 2))
(assert (not (= (select a1 x) 2)))
(check-sat)
第一个断言中的“存储”不影响第二个断言。我可以对阵列进行存储操作，从而导致阵列发生永久变化吗？我的意思是，如果我在数组上使用存储，那么数组将永远更改。例如，如果在我使用 '(store a1 x 2)' 之后，每次 (select a1 x) 都等于 2。有人知道吗？谢谢。
表达式(= (select (store a1 x 2) x) 2)等价于true。这是一个空洞的断言，因为数组理论公理之一是forall a,i,v: select(store(a,i,v), i) = v。因此，这个表达式只是公理（在 Z3 中内置）的一个实例，因此它是多余的。
也许，您打算断言(assert (= (select a1 x) 2)). 这个断言说数组在位置的值x是2。也就是说，Z3 生成的任何解都必须分配2给数组的这个位置a1。
请注意，在 Z3 中没有断言的“之前”和“之后”的概念或副作用。例如，表达式a = a + 1等价false于 Z3。用于将编程语言赋值编码到 Z3 中的一种常用技术为每个程序变量使用多个变量。每个“程序位置”一个变量。例如，代码块a = a + 1; b = 2*a; a = b + 1被编码为a_1 = a_0 + 1 and b_1 = 2*a_0 and a_2 = b_1 + 1. 以下文章包含更多示例/详细信息：http ://dl.acm.org/citation.cfm?id=1995394
如果您打算对程序中使用的数组更新进行编码，则应该有一个数组a1表示更新前的数组，一个数组a2表示更新后的数组。也就是说，我们写：(assert (= a2 (store a1 x 2)))，并将最后一个断言替换为 (assert(not (= (select a2 x) 2)))