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

[Tjark Weber]

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