title: Learning Z3py - Is there support for arrays and loops
body: <p>I'm going through Z3py and have a question with how to use the API in a couple specific cases.  The code below is a simplified version of something I would ultimately like to use Z3 for.  Some of my questions are:
    1. Is there a way to create an arbitrarily long array of values like the variable 'a' below?
    2. Can you access each element of the array in loops through Z3py?
    3. Is it possible to assign a result back into an original variable or is a new variable needed?  Will the conversion to CNF automatically add a unique id? (ie a += b)</p>
  
  <p>Overall, I'm lost on how to apply the Z3py API for something like the below algorithm where the solution depends on 'b'.  Any help or hints is/are appreciated, thank you.</p>
  
  <pre><code>import sys
  import struct
  
  a = "\xff\x33\x01\x88\x02\x11\x03\x55"
  b = sys.stdin.read(1) #a byte of user input - value 'a' is good
  c = ''
  d = ''
  
  for x in range(len(a)):
      c +=  struct.pack( 'B', int(a[x].encode('hex'), 16)^int(b.encode('hex'), 16) )
  
  print c.encode('hex')
  
  second = '\x23\x23'
  x = 0
  while x &lt; len(c):
      d += struct.pack( 'h', int(c[x:x+1].encode('hex'), 16)^int(second.encode('hex'), 16) )
      x += 2
  
  print d.encode('hex')
  
  if d == '\xbd\x23\x43\x23\x40\x23\x41\x23':
      print "Good"
  else:
      print "Bad"
  </code></pre>