title: Solve using Z3 solver a condition with a length of an arbitrary size array
body: <p>I'm learning Z3 solver. I have a question about Arrays and related conditions. In particular, I have to create Z3py code to solve the if condition below:</p>
  
  <pre><code>totalAccounts = [ 1, 2, 3, 4, 5 ]    
  
  def (myAccounts):
     cnt = len(myAccounts)
     if (cnt &gt; 10) doSomething()
  </code></pre>
  
  <p><code>myAccounts</code> is a list of Integers, subset of the list <code>totalAccounts</code>.
  The condition to pass is <code>cnt &gt; 10</code> which depends on the <em>length</em> of <code>myAccounts</code> list.</p>
  
  <p>I think I need to represent <code>myAccounts</code> as a Z3's Array and copy the values in <code>totalAccounts</code> on it using the function <code>Store</code>.</p>
  
  <pre><code>MYACCOUNTS = Array ('MYACCOUNTS', IntSort(), IntSort())
  I = Int('I')
  i = 0
  for elem in totalAccounts:
    MYACCOUNTS = Store(MYACCOUNTS, i, elem)
    i = i + 1
  </code></pre>
  
  <p>But I don't know how to represent the length of such array in creating the condition to add to the solver:</p>
  
  <pre><code>solver = Solver()
  solver.add( ??? &gt; 10 )
  </code></pre>
  
  <p>Am I doing it right?  </p>