code: def BitVecVal(value: int, size: int, annotations: Annotations = None) -> BitVec:
          
          raw = z3.BitVecVal(value, size)
          return BitVec(raw, annotations)
docs: Creates a new bit vector with a concrete value.