title: Checking all solutions for array (as-array) in Z3PY
body: <p>My problem is that I have to get all possible models for an array of the form <code>as-array</code>. The code I have done for this is the following:</p>
  
  <pre><code>s = Solver()
  check = s.check()
  while (str(check) == "sat"):
        mod = s.model()
        block = []
        for var in mod.decls():
           block.append(var() != mod[var])
        s.add(Or(block))
        check = s.check()
  </code></pre>
  
  <p><code>var</code> can take values of type <code>as-array</code> among others and when I run the line <code>s.add(Or(block))</code>, the next time I run the line <code>check = s.check</code> it returns unknown</p>
  
  <p>Is there any other way to do it?</p>
  
  <p>------- Edit -------</p>
  
  <p>I have found a way to get all possible models for an array of the form <code>as-array</code> that was the previous problem, the way I have done it is to create a variable that represents the size of the array and from i = 0 to i = n (where n is the size), make <code>a[i]!= x</code> being "a" the array and "x" the value that takes "a[i]".</p>
  
  <p>My problem now is that I have a datatype of the form "mk-pair" whose first argument is an array of the form <code>as-array</code> and an Integer that indicates the size of the array.</p>
  
  <p>When I get a model I have it in the form <code>mk-pair(as-array, 30)</code> (for example), being 30 the size of the array.</p>
  
  <p>The problem is that I can't find a way to obtain all the possible models, since if I deny the type of data (a != x, assuming that "a" is the datatype and "x" its value), it returns me unknown and if I do the first (as-array[0] != x), what I am really denying is <code>as-array</code>, not the variable "a"(which is of the form mk-pair(as-array, Int) ) and when I ask for models several times I get duplicate results.</p>
  
  <p>Any way to do this?</p>