parameters: (names, bv, ctx=None)
return_statement: return [BitVec(name, bv, ctx) for name in names]
docstring: Return a tuple of bit-vector constants of size bv.
  
      >>> x, y, z = BitVecs('x y z', 16)
      >>> x.size()
      16
      >>> x.sort()
      BitVec(16)
      >>> Sum(x, y, z)
      0 + x + y + z
      >>> Product(x, y, z)
      1*x*y*z
      >>> simplify(Product(x, y, z))
      x*y*z
docstring_summary: Return a tuple of bit-vector constants of size bv.
docstring_tokens: Return a tuple of bit - vector constants of size bv .
function: def BitVecs(names, bv, ctx=None):
      """Return a tuple of bit-vector constants of size bv.
  
      >>> x, y, z = BitVecs('x y z', 16)
      >>> x.size()
      16
      >>> x.sort()
      BitVec(16)
      >>> Sum(x, y, z)
      0 + x + y + z
      >>> Product(x, y, z)
      1*x*y*z
      >>> simplify(Product(x, y, z))
      x*y*z
      """
      ctx = _get_ctx(ctx)
      if isinstance(names, str):
          names = names.split(" ")
      return [BitVec(name, bv, ctx) for name in names]
function_tokens: def BitVecs ( names , bv , ctx = None ) : ctx = _get_ctx ( ctx ) if isinstance ( names , str ) : names = names . split ( " " ) return [ BitVec ( name , bv , ctx ) for name in names ]