Expand description
From the spec:
3.3 Identifiers
Identifiers are used mostly as function and sort symbols. When defining certain SMT-LIB theories it is convenient to have indexed identifiers as well. Instead of having a special token syntax for that, indexed identifiers are defined more systematically as the application of the reserved word _ to a symbol and one or more indices. Indices can be numerals or symbols.(8)
〈index 〉 ::= 〈numeral 〉 | 〈symbol 〉 〈identifier 〉 ::= 〈symbol 〉 | ( _ 〈symbol 〉 〈index 〉+ )