<SYSTEM_TASK:>
Solve the following problem using Python, implementing the functions described below, one line at a time
<END_TASK>
<USER_TASK:>
Description:
 def BitVecFuncVal( value: int, func_name: str, size: int, annotations: Annotations = None, input_: Union[int, "BitVec"] = None, ) -> BitVecFunc: """Creates a new bit vector function with a concrete value."""

        raw = z3.BitVecVal(value, size)
        return BitVecFunc(raw, func_name, input_, annotations)