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))
Как реализовать массив битовых векторов в API z3 Python