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

[Florian Lapschies]

On 06/17/2010 05:04 AM, Cesare Tinelli wrote:
>> By the way, is the symbol |xy| different from the symbol xy?
>>
> This is a good question. Quick answer: no.
>
> In the document, we actually meant them to be distinct. But we realize now that that conflicts with the goal of making SMT-LIB 2 a sublanguage of Common Lisp. In Common Lisp, the vertical bars are used as a quoting device, so |xy| and xy are in fact the same symbol.
>

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.

Regards,
Florian