[SMT-LIB] Grammar ambiguity for v2 attributes

[Christopher L Conway]

There appears to be an ambiguity in the grammar for v2 attributes:

   <attribute> ::= <keyword> | <keyword> <sexpr>
   <sexpr> ::= ... | <keyword> | ...

The input ":a :b :c" can be parsed as [hint: view in a fixed width font]

       :a        :b        :c
        |         |         |
    <keyword> <keyword> <keyword>
         \        |         |
          \    <sexpr>      |
           \     /          |
         <attribute>   <attribute>
                \       /
               <attribute>*

or

        :a        :b        :c
         |         |         |
     <keyword> <keyword> <keyword>
         |          \        |
         |           \    <sexpr>
         |            \     /
    <attribute>     <attribute>
             \       /
            <attribute>*

or

       :a           :b          :c
        |            |           |
     <keyword>   <keyword>   <keyword>
        |            |           |
    <attribute> <attribute> <attribute>
              \      |      /
               \     |     /
                <attribute>*

Is it the intention that set of attribute keywords will be well known,
as will their number and kind of values, and parser will be able to
handle them using context-sensitive rules? If so, what attributes are
included in the current SMT-LIB v2 benchmarks and what are their value
types?

Alternatively, are attributes allowed to have keyword values? Is it
the case that any existing attributes use keyword values?

Regards,
Chris