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

[Aaron Stump]

Hello, Tjark, Mate, and all.

I am sorry you ran into a problem with stack size.  We are actually not 
setting the stack limit explicitly in our jobscript.  What are you 
seeing that makes you think it is lower than what is shown with "ulimit 
-s" (namely, 8192KB)?  This value should have been something one could 
see with the VM instance (though we are due to update that in the next 
week or so, but I don't expect major changes).

Certainly one could ask for a higher stack limit than 8MB, and I would 
be happy to have us raise this or make it configurable.

Please let me know your thoughts on this.

Cheers,
Aaron

On 06/10/2016 04:29 AM, Tjark Weber wrote:
> 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