[SMT-LIB] minor updates to benchmarks

[Clark Barrett]

Could it be that your parser doesn't like "and" taking more than two arguments?
In fact, this is legal SMT-LIB format (if you check the grammar, you'll see
that "and" and "or" can take any non-zero number of arguments).

Other than that, I don't see a problem.  There is only a single instance of
"and", and according to my parser none of the instances of "bvand" have less
than 2 arguments.

As for a "flattened" format, the trick is to get something easier to debug
without dramatically increasing the file size.  I'm not sure about the best way
to do this.  I suggest you bring this up at the SMT-COMP discussion during the
workshop.

-Clark

> 
> Hi Clark,
> 
> My parser says something's wrong (supposedly, AND or BVAND has only one
> parameter) in QF_BV benchmark testcase15.stp.smt : 717394.
> 
> However, since that particular line has 20.222.495 characters (!), I
> couldn't find
> exactly the column where the problem starts.
> 
> BTW, this nesting style of dumping formulas is _really_ inconvenient for
> debugging. Would it be possible to flatten the benchmarks in the future
> (like in Spear format)?
> 
> On 6/18/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> > Also, the QF_BV tar file seems to have been missing some benchmarks.  Also, the
> > status and difficulty for the tacas07 benchmarks was unknown.  These have been
> > updated and the tar file now contains all the updated benchmarks.
> 
> Regards,
> 
> -- 
>         Domagoj Babic
> 
>         http://www.domagoj.info/
>