Re: [Smtcomp-discussion] benchmarks involving divide by zero

[Clark B. <ba...@cs...>]

Hi all,

I agree with David that the best thing to do is to remove the offending
benchmarks.  For a subset of the benchmarks, I believe we already have a
list from previous competitions (Morgan?).  For newer benchmarks, we will
have to find a way to determine this.

As for changing the standard, I suggest this be brought up at the SMT
workshop during the SMT-LIB discussion.  As there seems to be some
consensus, this will make a strong case for change.

-Clark


On Thu, Jun 12, 2014 at 7:57 AM, David Cok <dc...@gr...> wrote:

>  Florian - you are correct that some of the email on this topic in the
> last few days did not go to all participants. That is why I sent my email
> last evening to be sure there were no surprises to anyone. I discovered the
> problem in running some preliminary runs with historical solvers over the
> past week and Clark and Morgan did some detailed work to understand what
> the issue was.
>
> It appears to me that (a) SMT-LIB is well-defined on this point, (b) there
> is still some theoretical discussion happening, (c) not all solvers have
> adapted to the specific definitions in SMT-LIB, and (d) we are just three
> days away from the deadline, so it is unreasonable to expect major changes
> in existing tools.
>
> Thus, as lead organizer, I am inclined to propose that the benchmarks at
> issue be recused from the competition.
> - I'm willing to hear discussion pro and con on that point.
> - I also need to know which benchmarks are the ones at issue.
>
> David
>
>
>
> On 6/12/2014 8:26 AM, Florian Lapschies wrote:
>
>
>
>
> I've updated new versions with corrected status attributes for the
> QF_BV/spear/w_get benchmarks (corrected according to the current SMT-LIB
> standard).  As mentioned in the discussion thread, the other benchmarks in
> question appear to be labeled correctly - it is just that some solvers do
> not give the right answer.
> -Clark
>
>
> I searched my SMT-COMP mails that I received the last couple of days and
> can't find any information about these other benchmarks. Have the authors
> of these solvers been contacted?
>
> Best regards,
> Florian
>
>
>