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

[Tjark Weber]

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