[SMT-LIB] Use of @ and . in a quoted symbol

[Delcypher]

Hi,

Thanks for the reply.

On 25 April 2015 at 17:49, Tinelli, Cesare <cesare-tinelli at uiowa.edu> wrote:
> Dan,
>
> On Page 21 of the SMT-LIB 2.0 document you have
>
> "Following Common Lisp's convention, enclosing a simple symbol in vertical bars does not produce a new symbol. This means for instance that abc and |abc| are the same symbol."
>
> For the same reasons, |.x| and .x  are the same symbol. That is why CVC4 rejects |.x| in the declaration below.

Ah I was only looking at

```
Members of the symbol category starting with of the characters @ and .
are reserved
for solver use.
```

based on that and the grammar written above it, they imply ``|.x|`` is
not reserved (the first character is ``|``) where as ``.x`` (the first
character is ``.``) is. Perhaps the wording could be improved there?

Thanks,
Dan.