Creates a bit-vector symbol (i.e., a variable).

    If you want to specify the maximum or minimum value of a normal symbol that is not part of value-set analysis, you
    should manually add constraints to that effect. **Do not use ``min`` and ``max`` for symbolic execution.**

    :param name:            The name of the symbol.
    :param size:            The size (in bits) of the bit-vector.
    :param min:             The minimum value of the symbol, used only for value-set analysis
    :param max:             The maximum value of the symbol, used only for value-set analysis
    :param stride:          The stride of the symbol, used only for value-set analysis
    :param uninitialized:   Whether this value should be counted as an "uninitialized" value in the course of an
                            analysis.
    :param bool explicit_name:   If False, an identifier is appended to the name to ensure uniqueness.
    :param bool discrete_set: If True, a DiscreteStridedIntervalSet will be used instead of a normal StridedInterval.
    :param int discrete_set_max_card: The maximum cardinality of the discrete set. It is ignored if discrete_set is set
                                      to False or None.

    :returns:               a BV object representing this symbol.

def BVS(name, size, min=None, max=None, stride=None, uninitialized=False,  #pylint:disable=redefined-builtin
        explicit_name=None, discrete_set=False, discrete_set_max_card=None, **kwargs):
    """
    Creates a bit-vector symbol (i.e., a variable).

    If you want to specify the maximum or minimum value of a normal symbol that is not part of value-set analysis, you
    should manually add constraints to that effect. **Do not use ``min`` and ``max`` for symbolic execution.**

    :param name:            The name of the symbol.
    :param size:            The size (in bits) of the bit-vector.
    :param min:             The minimum value of the symbol, used only for value-set analysis
    :param max:             The maximum value of the symbol, used only for value-set analysis
    :param stride:          The stride of the symbol, used only for value-set analysis
    :param uninitialized:   Whether this value should be counted as an "uninitialized" value in the course of an
                            analysis.
    :param bool explicit_name:   If False, an identifier is appended to the name to ensure uniqueness.
    :param bool discrete_set: If True, a DiscreteStridedIntervalSet will be used instead of a normal StridedInterval.
    :param int discrete_set_max_card: The maximum cardinality of the discrete set. It is ignored if discrete_set is set
                                      to False or None.

    :returns:               a BV object representing this symbol.
    """

    if stride == 0 and max != min:
        raise ClaripyValueError("BVSes of stride 0 should have max == min")

    encoded_name = None
    if type(name) is bytes:
        encoded_name = name
        name = name.decode()
    if type(name) is not str:
        raise TypeError("Name value for BVS must be a str, got %r" % type(name))

    n = _make_name(name, size, False if explicit_name is None else explicit_name)

    if not discrete_set:
        discrete_set_max_card = None

    return BV('BVS', (n, min, max, stride, uninitialized, discrete_set, discrete_set_max_card), variables={n},
              length=size, symbolic=True, eager_backends=None, uninitialized=uninitialized, encoded_name=encoded_name,
              **kwargs)