title: Z3: How to select 4 bytes from array of 8-bits?
body: <p>With Python Z3, I have an array of bytes, and can use Select to read 1 byte like below.</p>
  
  <pre><code>MI = BitVecSort(32)
  MV = BitVecSort(8)
  Mem = Array('Mem', MI, MV)
  
  pmt = BitVec('pmt', 32)
  pmt2 = BitVec('pmt2', 8)
  
  g = True
  g = And(g, pmt2 == Select(Mem, pmt))
  </code></pre>
  
  <p>So far, this is OK. However, now I want to read 4 bytes out of Mem array, like below.</p>
  
  <pre><code>t3 = BitVec('t3', 32)
  g = And(g, t3 == Select(Mem, pmt))
  </code></pre>
  
  <p>This turns out to be wrong, because t3 is 32-bit, not 8-bits, while Mem is the array of 8-bits.</p>
  
  <p>The question is: How can I use Select to read out 4 bytes, but not 1 byte in the above example? </p>
  
  <p>I suppose that I can create a new function to read out 4 bytes, lets say Select4(), but I am not sure how to create a function in Z3 python.</p>
  
  <p>Thank you so much!</p>