[SMT-LIB] Question on QF_NIA Benchmarks

[Andrej Dyck]

Hello,

I'm working with the SMT-LIB QF_NIA benchmarks available on the SMT-LIB 
website and wondered why my parser doesn't parse the benchmarks from 
"calypto" (QF_NIA) and found out, that the benchmarks contain asserts like:
  (assert (let (?v_0 (not (< 2 P_2))) (= (+ (* 1073741824 dz) rz) (- (* 
(ite ?v_0 P_3 P_5) P_4) (ite ?v_0 (* P_3 P_4) (* P_5 P_4)))))) [*]
But the grammar, as formalized in the documentation of SMT-LIB 2.0 (page 
23 or page 72), for terms looks like this:
  <var_binding> ::= (<symbol><term>)
  <term> ::= ( let (<var_binding>+) <term> )
So the let-expression should look like this:
  (let ((x1 t1)...(xn tn)) t) [Example from page 24, notice the nesting 
depth!]

Now I'm wondering if the benchmarks have been translated in a wrong way 
or do I have missed something in the documentation, that allows terms 
like in [*].

Regards,
  Andrej Dyck