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

[Tjark Weber]

On Wed, 2016-05-25 at 09:50 +0200, David Deharbe wrote:
> This request sounds perfectly reasonable and poses a problem.
> 
> In my opinion the changes should be coordinated with the SMT-LIB
> maintainers. [...]

The situation is even more convoluted. The SMT-COMP benchmark scrambler
currently does not pass 'set-info' commands to the solver. At least in
the case of the :source and :status attributes, this is for good
reason.

The scrambler could be modified to pass on 'set-info :smt-lib-version'
commands only; but the SMT-COMP rules postulate that set-option and
set-logic commands come first in benchmarks.

I will investigate whether it would be feasible to provide all
benchmarks in a form that is compatible with both 2.0 and 2.5.
Otherwise, we may have to declare benchmarks that cause parsing
problems/ambiguities ineligible for SMT-COMP 2016.

Best,
Tjark