code: def Sum(*args: BitVec) -> BitVec:
      
      raw = z3.Sum([a.raw for a in args])
      annotations = []  # type: Annotations
      bitvecfuncs = []
  
      for bv in args:
          annotations += bv.annotations
          if isinstance(bv, BitVecFunc):
              bitvecfuncs.append(bv)
  
      if len(bitvecfuncs) >= 2:
          return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=annotations)
      elif len(bitvecfuncs) == 1:
          return BitVecFunc(
              raw=raw,
              func_name=bitvecfuncs[0].func_name,
              input_=bitvecfuncs[0].input_,
              annotations=annotations,
          )
  
      return BitVec(raw, annotations)
docs: Create sum expression.
  
      :return: