code: def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
      
      result = []
      if not expression.children() and not isinstance(expression, z3.BitVecNumRef):
          result.append(expression)
      for child in expression.children():
          c_children = _get_expr_variables(child)
          result.extend(c_children)
      return result
docs: Gets the variables that make up the current expression
      :param expression:
      :return: