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

Dejan Jovanović dejan.jovanovic at sri.com
Mon May 23 19:33:55 EDT 2016


Hi Tjark,

My reading of your message is the following:
* All old benchmarks are in smtlib 2.0 format
* New benchmarks are in smtlib 2.5 format

Is this correct?

If so, would it be possible to get a list of new benchmarks (that might be
problematic). This would help with the testing, we don't want to run the
whole library.

Thanks, Dejan

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

> Dear SMT-COMP participants,
>
> The 2016-05-23 SMT-LIB release is now available at
> https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=161238
>
> Thanks to Clark Barrett and everyone who submitted or cleaned up
> benchmarks!
>
> This SMT-LIB release still contains a large number of benchmarks with
>   'set-info :smt-lib-version 2.0'
> in addition to a smaller number of benchmarks with
>   'set-info :smt-lib-version 2.5'.
>
> Most of the benchmarks are compatible with both 2.0 and 2.5. Moreover,
> none of the commands or options newly introduced in 2.5 will be used in
> competition benchmarks. However, there are incompatibilities that could
> be relevant for SMT-COMP; notably the use of "" as an escape sequence
> in string literals, and the use of Unicode characters. Please see the
> SMT-LIB standard for details.
>
> For SMT-COMP 2016, this unfortunately means that solvers will need to
> support (the relevant subset of) both formats. Apologies for the
> inconvenience!
>
> Best,
> Tjark
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>


More information about the SMT-COMP mailing list