小编leo*_*onh的帖子

在使用SMTLIB阵列时,我注意到Z3对该理论的理解与我的理解之间存在差异.我正在使用SMTLIB阵列理论[0],它可以在官方网站上找到[1].

我认为用一个简单的例子可以很好地说明我的问题.

(store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0)
       (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)

第一个数组应该在索引1返回2,对于所有其他索引应该返回0,第二个数组应该在索引0处返回1,在索引1处返回2,对于所有其他索引应该返回0.select在索引0处调用似乎证实了这一点:

(assert
    (=
        (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0)
        0
    )
)
(assert
    (=
        1
        (select        (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)      0)
    )
)

sat两个Z3都返回.

(assert
    (=
        (select (store (store …