code: def Extract(high: int, low: int, bv: BitVec) -> BitVec:
      
      raw = z3.Extract(high, low, bv.raw)
      if isinstance(bv, BitVecFunc):
          # Is there a better value to set func_name and input to in this case?
          return BitVecFunc(
              raw=raw, func_name=None, input_=None, annotations=bv.annotations
          )
  
      return BitVec(raw, annotations=bv.annotations)
docs: Create an extract expression.
  
      :param high:
      :param low:
      :param bv:
      :return: