[SMT-COMP] StarExec questions

François Bobot francois.bobot at cea.fr
Wed Jun 14 03:17:58 EDT 2017

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

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