[SMT-COMP] StarExec questions
francois.bobot at cea.fr
Wed Jun 14 03:17:58 EDT 2017
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):
But if you take for example the first one, the solver answered unsat:
And the status of the benchmark is unknown:
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,
More information about the SMT-COMP