[SMT-LIB] Question on QF_NIA Benchmarks

[Clark Barrett]

Andrej,

In fact, we just discovered the same problem.  This is due to a bug in our
translator.  We have fixed it and will post a new version of the benchmarks
shortly.

-Clark


On Wed, May 5, 2010 at 9:23 AM, Andrej Dyck <andrej.dyck at rwth-aachen.de>wrote:

> 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
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>