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

Vijay Ganesh vijay.ganesh at uwaterloo.ca
Tue Jun 14 05:09:05 EDT 2016


Sounds good, Tjark.

I will let Mate respond to the June 17th deadline, since he is doing most of the hacking. 

Thanks again!

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

________________________________________
From: Tjark Weber [tjark.weber at it.uu.se]
Sent: Monday, June 13, 2016 7:04 PM
To: Vijay Ganesh; Mate Soos
Cc: David Deharbe; Sylvain Conchon; smt-comp at cs.nyu.edu; jliang at gsd.uwaterloo.ca
Subject: Re: [SMT-COMP] SMT-COMP 2016: Application Track Testing

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



More information about the SMT-COMP mailing list