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

[Christoph Wintersteiger]

Hi all,

I think for the purpose of the competition this little detail really doesn't make much of a difference. We could simply sed "s/\"/_/g" all of them before passing them to the solvers. Or, perhaps even easier, just strip the whole (set-info :source ...) command. I'm not aware of any such issues in other commands, at least not in the SMTLIB benchmarks.

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-comp-bounces at cs.nyu.edu [mailto:smt-comp-bounces at cs.nyu.edu] On Behalf Of Tjark Weber
Sent: 25 May 2016 15:25
To: David Deharbe <david.deharbe at clearsy.com>; Bruno Dutertre <bruno.dutertre at sri.com>
Cc: Sylvain Conchon <Sylvain.Conchon at lri.fr>; smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] SMT-COMP 2016: Benchmarks in 2.0 and 2.5 Formats

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

_______________________________________________
SMT-COMP mailing list
SMT-COMP at cs.nyu.edu
https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fcs.nyu.edu%2fmailman%2flistinfo%2fsmt-comp&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c9ae01be1f0ab4322a1ef08d384a8706a%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=rJWHljdQidHS0rYSLyschomHj%2bpkaCgYbMrOH3ZVy08%3d