def BitVecVector(prefix, sz, N):
    """Create a vector with N Bit-Vectors of size sz"""
return [BitVec('%s__%s' % (prefix, i), sz) for i in range(N)]
How to implement array of bitvectors in z3's Python APIs