SMTLIB array theory oddity in Z3

Question

While using SMTLIB arrays, I noticed a difference between Z3's understanding of the theory and mine. I am using the SMTLIB array theory [0] which can be found on the official website [1].

I think my problem is best illustrated with a simple example.

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

The first array should return 2 at index 1 and 0 for all other indices, the second should return 1 at index 0, 2 at index 1, and 0 for all other indices. Calling select at index 0 seems to confirm this:

(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 returns sat for both.

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

As expected, Z3 (in case it matters, I am using version 3.2 on linux-amd64) answers unsat in this case. Next, let's compare these two arrays:

(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 tells me sat, which I interpret as "these two arrays compare equal". However, I would expect these arrays not to compare equal. I base this on the SMTLIB array theory, which says:

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

So, in plain English this would mean something like "Two arrays shall compare equal if, and only if they are equal for all indices". Can anybody explain this to me? Am I missing something or misunderstanding the theory? I'd be grateful for any thoughts that you might have on this issue.

Best regards, Leon

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

Answer 1

Thanks for reporting the problem. This is a bug in the array preprocessor. The preprocessor simplifies array expressions before the actual solver is invoked. The bug affects only problems that use constant arrays (e.g., ((as const (Array Int Int)) 0)). You can workaround the bug by not using constant arrays. I fixed the bug, and the fix will be available in the next release.