[SMT-COMP] StarExec questions

[Tjark Weber]

François,

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.

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?

Best,
Tjark