[SMT-COMP] StarExec questions

Tjark Weber tjark.weber at it.uu.se
Tue Jun 13 09:20:08 EDT 2017


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?


More information about the SMT-COMP mailing list