a = BitVec('a', 8)
DomVect = [BitVec('DomVect_%s' % i, 8) for i in range(16)]
print(DomVect)
print(DomVect[15])

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)]
print(BitVecVector('A', 8, 32))
How to implement array of bitvectors in z3's Python APIs