[SMT-LIB] New SMT-LIB release for SMT-COMP 2011---includes fixes, additions

Tjark Weber tjark.weber at gmx.de
Fri May 20 14:02:26 EDT 2011


Morgan,

On Mon, 2011-05-16 at 00:25 -0400, Morgan Deters wrote:
> Please let me know if there are any benchmark compliance issues, [...]

There is another compliance issue in mcm/{162,164,166,170}.smt2 (and
perhaps other benchmarks):  These benchmarks apply 'or' to a single
argument (e.g., at line 2859f. in mcm/162.smt2).  The description
of :left-assoc in Section 3.7 of the SMT-LIB standard leads me to
believe that this is not valid.

Kind regards,
Tjark




More information about the SMT-LIB mailing list