[SMT-COMP] SMT-COMP 2016: Benchmarks in 2.0 and 2.5 Formats

[Dejan Jovanović]

Tjark,

There are thousands of new benchmarks, particularly in the bit-vector
category (e.g QF_BV/Sage2 17471 benchmarks) . As far as we saw they are
marked as "unknown".

You haven't really responded to the "unknown" status issue. This is
important. From the discussion and talking with people it's clear that
relying on "known" benchmarks only is detrimental to competition.

Can you please give the final word on this. Will only the "known"
benchmarks be used in the competition?

Best, Dejan

On Wed, May 25, 2016 at 3:03 PM Tjark Weber <tjark.weber at it.uu.se> wrote:

> On Wed, 2016-05-25 at 13:41 -0700, Clark Barrett wrote:
> > I think the situation is actually much better than advertised.  I
> > believe that the *only* feature of smt-lib 2.5 (versus 2.0) being
> > used is representing quotes-within-quotes as "" instead of \" and
> > this only happens in a few benchmarks and only in their source
> > attribute.
> >
> > So, if the SMT-COMP scrambler strips the source attribute, then *all*
> > benchmarks should be fully smt-lib 2.0 compliant.  Please do let me
> > know if anyone finds a counter-example to this claim, but if it is
> > true, then I think there should not be an version issue for the
> > competition.
>
> As far as I can see after grepping over the entire SMT-LIB, this
> accurately describes the current situation. Moreover, version 2.0
> escape sequences \" and \\ do not seem to appear anywhere.
>
> The competition scrambler (which is now available at
> http://smtcomp.sourceforge.net/2016/tools.shtml) has been revised to
> support "" within strings. Since the scrambler strips the :source
> attribute, solvers should never see "" as an escape sequence. Thus,
> this difference between 2.0 and 2.5 should be immaterial for the
> competition.
>
> Please let me know if your own testing reveals any related issues.
>
> Best,
> Tjark
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>