[SMT-LIB] Comments to the new SMT-LIB standard

[Morgan Deters]

Hi Florian,

On Fri, Jun 18, 2010 at 2:42 AM, Florian Lapschies <
florian.lapschies at googlemail.com> wrote:

> I would like to point out that the newly added conformance-checking test
> QF_BV/check2/symbols.smt2 still requires |xy| and xy to be different
> symbols.
>
> In addition, there are some benchmarks in QF_BV/brummayerbiere* that
> contain '|' in symbols that start and end with '|'. One example is
> QF_BV/brummayerbiere/nextpoweroftwo016.smt2.
>

Thanks for the reports.  In fact, these two issues have been discovered and
the fixes have already posted.  An announcement is forthcoming.

Thanks,
Morgan
-- 
Morgan Deters
mdeters at gmail.com