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

[Mate Soos]

Hi Tjark,

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


Although I don't think re-running those 25 problems with a larger stack
limit would case any inconsistencies in performance, I understand that
things can get political. Let's try fixing the problem up for next time
:) I'm talking with Aaron, thanks for putting me in contact!

Thanks again for organising, it was fun!

Mate


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5524 bytes
Desc: S/MIME Cryptographic Signature
URL: </pipermail/smt-comp/attachments/20160611/f03a9df8/attachment-0001.p7s>