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