[SMT-COMP] SMT-COMP 2016: Application Track Testing

[Vijay Ganesh]

Dear Tjark, David, and Aaron,

Given that we have a much better understanding of the problem, and that it can be easily fixed, I would like to suggest the following:

Can we run all mt solvers, with the appropriate configuration, only on those instances for which the problem was observed?

This I think would be a fair compromise, and highly doable in terms of resources since the number of instances on which stp-mt failed is fairly small. You won't have to re-run all the solvers on all instances or a single solver on all instances with a different configuration. 

As Clark mentioned this problem was known already, and for some reason was not taken into account during the setup of the competition this year.

We would really appreciate if you are able to reconsider your decision. Thanks!

Cheers,
Vijay Ganesh.
https://ece.uwaterloo.ca/~vganesh

________________________________________
From: Tjark Weber [tjark.weber at it.uu.se]
Sent: Friday, June 10, 2016 5:29 AM
To: Mate Soos
Cc: David Deharbe; Sylvain Conchon; Vijay Ganesh; smt-comp at cs.nyu.edu; jliang at gsd.uwaterloo.ca; Aaron Stump
Subject: Re: [SMT-COMP] SMT-COMP 2016: Application Track Testing

Mate,

On Tue, 2016-06-07 at 01:32 +0100, Mate Soos wrote:
> By the way, we have observed a strange crash on StarExec with the
> multi-threaded executable (stp-cms-mt-2016) of the main competition.
> The corresponding executable works fine on our machines, and in
> deeper inspection it seems that StarExec limits the stack size to
> lower than what is on our machines or the distributed official
> StarExec OVA. This causes our solver to crash.
>
> https://www.starexec.org/starexec/secure/details/pairsInSpace.jsp?typ
> e=unknown&sid=560017&configid=158183&stagenum=1
>
> This is not reproducible with the OVA distributed by StarExec, as
> it's a runtime setting by the execution environment (hence it took us
> a week to track it down). I'm wondering if it would be possible to
> re-run those 28 SMTLIB2 inputs with a larger stack on StarExec?

Thank you for taking the time to track this down. It is unfortunate
that stp-cms-mt-2016 was affected in this way, and if your analysis is
correct, I agree that a higher stack limit would be desirable for
future competitions.

However, we have decided that it would not be fair to re-run one solver
with a different StarExec configuration as part of SMT-COMP 2016: we do
not know how other competing solvers would be affected by such a change
to the execution environment (and at this point it is not feasible to
re-run all job pairs). To ensure comparability of results and fairness
of the competition, we believe it is important that all solvers were
run within the same environment.

Note also that the stack limit is not under our (the competition
organizers') immediate control, but is determined by the StarExec
environment. I am therefore cc'ing this email to Aaron Stump.

Best,
Tjark