def declare_array(a, bv1, bv2):
    """
    Declares an SMT2 array represented as a map
    from a bit vector to another bit vector.
    :param a: array name
    :param bv1: SMT2 bit vector
    :param bv2: SMT2 bit vector
    """
    return '(declare-fun {} () (Array {} {}))'.format(a, bv1, bv2)
