[SMT-LIB] minor updates to benchmarks

Domagoj Babic babic.domagoj at gmail.com
Tue Jun 19 17:19:23 EDT 2007


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/


More information about the SMT-LIB mailing list