The particular concrete syntax implemented by the Parser and the Printer is the S-expression syntax described in the SMT-LIB v.2 documentation. In this syntax, all abstract quantities are rendered as S-expressions: either individual tokens, or a sequence consisting of a left-parenthesis, a series of whitespace-separated S-expressions, and a closing right-parenthesis. The whitespace separating a series of S-expressions may be spaces, tabs, new-line or carriage-return characters.

The allowed tokens are

• numeral - either a '0' or a sequence of digits starting with a non-zero digit
• decimal - a numeral followed by a period followed by a sequence of digits
• binary literal - the characters '#b' followed by a sequence of '0' and '1' digits
• hex literal - the characters '#x' followed by a sequence of upper- or lower-case hex digits
• string literal - a '"'-enclosed sequence of printable characters, with a backslash included as '\\' and an embedded quote as '\"'
• symbol - a sequence, starting with a non-digit, of digits, upper and lower case letters and these punctuation characters: +-*/_=%?!.$~&^<>@ Some character sequences that would be symbols are instead reserved words.
• quoted symbol - a sequence of any printable or whitespace characters beginning and ending with vertical bars (|).
• keywords - a colon followed by a sequence of printable characters allowed in unquoted symbols
• reserved words - some character sequences are reserved and not allowed to be used as symbols. These are
  forall exists let as _ ! par NUMERAL DECIMAL STRING
  and the pre-defined commands:
  assert check-sat declare-fun declare-sort define-fun define-sort exit get-assertions get-assignment get-info get_option get-proof get-unsat-core get-value pop push set-info set-logic set-option

A command has the form ( command-name arguments... )
in which the command-name is a symbol or reserved word naming the command and the arguments are also S-expressions of particular forms, depending on the command.

The logical formulas that are asserted and reasoned about by an SMT solver also are S-expressions. An expression can in general take one of the following forms, though the particular logic in effect may limit some of the syntax and will specify which functions are defined:

• a numeral, decimal, binary, hex, or string literal
• a symbol (including quoted symbols), both of which are simple forms of identifiers
• a parameterized identifier: ( _ symbol series-of-numerals )
• a function evaluation: ( identifier arguments... )
• a named expression: ( ! expression :named symbol )
• universal quantification: ( forall ( series-of-symbol-sort-pairs ) expression )
• existential quantification: ( exists ( series-of-symbol-sort-pairs ) expression )
• let expression: ( let ( series-of-symbol-expression-pairs ) expression )