def footer(id1, id2 = None):
    """
    Build SMT formula footer

    Args:
        id1 (str): ID of policy 1 in SMT formula
        id2 (str, optional): ID of policy 2 in SMT formula. Defaults to None.

    Returns:
        str: SMT footer
    """

    smt = '(assert {}.allows)\n'.format(id1)

    if id2:
        smt += '(assert (or {0}.denies {0}.neutral))\n'.format(id2)

    smt += '(check-sat)\n'
    smt += '(get-model)\n'

    return smt