def array_to_logic(a, counter, aut):
    """Return logic formula for Boolean array `a`.

    No array bounds produced.
    Instead, if `(counter < 0) or (counter >= len(a) - 1)`,
    then select `a[-1]`.
    Therefore, array bounds *must* be added separately.

    @param a: `list` of elements
    @param counter: name of index variable
    """
    bdd = aut.bdd
    r = a[-1]
    for i, x in enumerate(a[:-1]):
        s = '{counter} = {i}'.format(counter=counter, i=i)
        u = aut.add_expr(s)
        r = bdd.ite(u, x, r)
    return r