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

[Bruno Dutertre]

On 05/23/2016 03:22 PM, Tjark Weber 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'.
>

Could you please make sure that the (set-info :smt-lib-version ...)
occurs first in the benchmarks, or at least before any string literal?
This is currently not the case.

Example:

non-incremental/QF_BV/brummayerbiere/nextpoweroftwo512.smt2

(set-logic QF_BV)
(set-info :source "
We verify the correctness of the ""next power of 2 algorithm""
from the book ""hacker's delight"" (Warren Jr., Henry).

Algorithm:
int next_power_of_2 (int x)
{
   int i;
   x--;
   for (i = 1; i < sizeof(int) * 8; i = i * 2)
   x = x | (x >> i)
   return x + 1;
}

Bit-width: 512

Contributed by Robert Brummayer (robert.brummayer at gmail.com).
")
(set-info :smt-lib-version 2.5)
(set-info :category "crafted")
(set-info :status unsat)
...

Thanks,

Bruno


> 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
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4049 bytes
Desc: S/MIME Cryptographic Signature
URL: </pipermail/smt-comp/attachments/20160524/62554e75/attachment.p7s>