Необычность теории массивов SMTLIB в Z3

Используя массивы 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)

Первый массив должен возвращать 2 в индексе 1 и 0 для всех остальных индексов, второй должен возвращать 1 в индексе 0, 2 в индексе 1 и 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)
    )
)

Z3 возвращает sat для обоих.

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

Как и ожидалось, Z3 (если это важно, я использую версию 3.2 на linux-amd64) в этом случае отвечает unsat . Затем давайте сравним эти два массива:

(assert
    (=
        (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)
    )
)

Z3 сообщает мне sat , что я интерпретирую как «эти два массива сравниваются одинаково». Однако я ожидал, что эти массивы не будут сравниваться равными. Я основываю это на теории массивов SMTLIB, которая гласит:

- (forall ((a (Array s1 s2)) (b (Array s1 s2)))
    (=> (forall ((i s1)) (= (select a i) (select b i)))
            (= a b)))

Итак, на простом английском языке это будет означать что-то вроде «Два массива будут сравниваться равными, если и только если они равны для всех индексов». Кто-нибудь может мне это объяснить? Я что-то упускаю или неправильно понимаю теорию? Буду признателен за любые мысли, которые могут у вас возникнуть по этому поводу.

С уважением, Леон

[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 [1] http: // smtlib.org