code: def BitVecFuncSym(
          name: str,
          func_name: str,
          size: int,
          annotations: Annotations = None,
          input_: Union[int, "BitVec"] = None,
      ) -> BitVecFunc:
          
          raw = z3.BitVec(name, size)
          return BitVecFunc(raw, func_name, input_, annotations)
docs: Creates a new bit vector function with a symbolic value.