title: SMTLIB array theory oddity in Z3
body: <p>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].</p>
  
  <p>I think my problem is best illustrated with a simple example.</p>
  
  <pre><code>(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)
  </code></pre>
  
  <p>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 <code>select</code> at index 0 seems to confirm this:</p>
  
  <pre><code>(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)
      )
  )
  </code></pre>
  
  <p>Z3 returns <code>sat</code> for both.</p>
  
  <pre><code>(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)
      )
  )
  </code></pre>
  
  <p>As expected, Z3 (in case it matters, I am using version 3.2 on linux-amd64) answers <code>unsat</code> in this case. Next, let's compare these two arrays:</p>
  
  <pre><code>(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)
      )
  )
  </code></pre>
  
  <p>Z3 tells me <code>sat</code>, 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:</p>
  
  <pre><code>- (forall ((a (Array s1 s2)) (b (Array s1 s2)))
      (=&gt; (forall ((i s1)) (= (select a i) (select b i)))
              (= a b)))
  </code></pre>
  
  <p>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.</p>
  
  <p>Best regards,
  Leon</p>
  
  <p>[0] <a href="http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2">http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2</a>
  [1] <a href="http://smtlib.org">http://smtlib.org</a></p>