title: Z3 Python Check whether pairs are distinct
body: <p>I have a 2 matrices, each of them are 3 by 3 (call them M1 and M2, each of their entries are of type Int in Z3.  I need to add the constraint that says all pairs of the form ([M1[i][j], M2[i][j]) are distinct (i and j are arbitrary indices for the matrix).</p>
  <p>In other words,</p>
  <pre><code>if   (i1,j1) != (i2,j2) 
  then ([M1[i1][j1], M2[i1][j1]) != ([M1[i2][j2], M2[i1][j2])
  </code></pre>
  <p>I tried making an array of all the pairs, called array, then using Distinct(array), but this doesn't seem to work since I get an error saying</p>
  <p>&quot;At least one of the arguments must be a Z3 expression&quot;</p>
  <p>Is there a way to see if 2 pairs of integers are distinct in Z3 for Python? And if not what's a good way to enable the constraint that the pairs described above are distinct?</p>