[SMT-LIB] minor updates to benchmarks

[Domagoj Babic]

Hi,

On 6/19/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> 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...

Hmm.. I had the same problem converting from the Spear format (which also
allows subexpression sharing) to SMT. The simplest solution is to introduce
fresh variables. Is there any particular reason why that was infeasible for that
particular instance?

Regards,

-- 
        Domagoj Babic

        http://www.domagoj.info/