[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