[SMT-COMP] StarExec questions

[François Bobot]

Hi Tjark,

Le 13/06/2017 à 15:20, Tjark Weber a écrit :
> On Tue, 2017-06-13 at 13:44 +0200, François Bobot wrote:
>> Yes it is very confusing that the main postprocessors (SMT-COMP *)
>> answers wrong when a prover solves a benchmark marked as unknown. Does
>> some people uses other post-processors?
>
> Note that the post-processor merely identifies the solver's answer
> (e.g., unknown) based on the solver's output.

Oh I see. So the post-processor is not to be blamed and the problem is perhaps that the 
expected-result is `starexec-unknown`.

>
> Whether this answer is shown as correct is a determination that is made
> by the StarExec framework. (For the competition, we will use our own
> scripts to make this determination independently.)


>
> 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

In fact I think people that are used to star-exec knows that they shouldn't be afraid of these 
wrongs (even more when all the compared provers have some), but when you are using a job as an 
artefact for a paper reviewers and readers could be confused. I should have added a note about that 
in the paper, however it would be great to not have to.


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?

Thanks a lot for the organization,

-- 
François