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

[Tjark Weber]

Vijay (et al.),

On Sun, 2016-06-12 at 18:26 +0000, Vijay Ganesh wrote:
> 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.

I realize that it can be disappointing to be affected by such an issue.

However, if I understand the situation correctly, (i) the issue could
have been noticed (at least in principle) before the competition
through testing on the StarExec cluster (albeit not on the VM), and
(ii) the results of the competition job accurately reflect the
capabilities of the solver version that had been submitted by the final
solver deadline.

Under these circumstances, I do not believe that it would be fair to
other competitors to enter a fixed version of STP-cms-mt into the 2016
competition.

Nonetheless, if you want to make such a version (that explicitly sets
its per-thread stack limit) available to us, we would be happy to run
it non-competitively. Specifically, we would announce its results
together with the competition results, but it would not be eligible to
be officially recognized as winner.

We would need this version by Friday (June 17) at the latest.

Best,
Tjark