[SMT-LIB] minor updates to benchmarks

[Clark Barrett]

You may be interested to know the reason for this.  Originally, all but the
last one of these were assumptions.  However, when I translated from CVC to
SMT-LIB format, the translation blew up.  After some investigation, I
discovered this was because CVC format allows expression sharing across
assumptions whereas SMT-LIB format does not.  Thus, the only way to translate
them was to pile all of the assumptions into the formula as one big AND.  This
is one of the format issues I hope to discuss during the workshop...

-Clark

> 
> Hi,
> 
> On 6/18/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> > 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).
> 
> Right, it's an AND with 297813 operands :-).
> 
> Anyways, all QF_BV benchmarks parse correctly now...
> 
> Regards,
> 
> -- 
>         Domagoj Babic
> 
>         http://www.domagoj.info/
>