[SMT-COMP] StarExec questions

[Tjark Weber]

François,

On Wed, 2017-06-14 at 09:17 +0200, François Bobot wrote:
> Oh I see. So the post-processor is not to be blamed and the problem is perhaps that the 
> expected-result is `starexec-unknown`.

> > Do you have a link to a job/job pair that shows the confusing behavior?
> 
> All these results are said to be wrong (a job with a 4s timeout just for checking parsing):
> https://www.starexec.org/starexec/secure/details/pairsInSpace.jsp?type=wrong&sid=805276&configid=219863&stagenum=1
> 
> But if you take for example the first one, the solver answered unsat:
> 
> https://www.starexec.org/starexec/secure/details/pair.jsp?id=290636161
> 
> And the status of the benchmark is unknown:
> 
> https://www.starexec.org/starexec/secure/details/benchmark.jsp?id=4688215

I would encourage you to submit a bug report/feature request on the
StarExec support forum. In my opinion, when a benchmark's
expected-result is starexec-unknown, it would be more reasonable to
classify any solver answer as "unknown" in StarExec.

> PS: I didn't find in the SMT-COMP rules where to send the final/fixed version of a prover. Should we 
> use again the google webform?

If you update your solver, please send us (i.e., the competition
organizers, and in particular me) an email with the StarExec id of the
final version.

Best,
Tjark