title: Resize BitVec in z3 [Python]
body: <p>I need to symbolize an unknown length byte string in z3. I see two options: symbolize each byte necessary, then concat bytes when constraints need to be applied, or symbolize one long bytestring, extracting portions when constraints need to be applied.</p>
  
  <p>One long bytestring seems more convenient, but it would need to be resized when a larger amount of data is needed. Does z3 have a way to do this?</p>