[SMT-COMP] StarExec questions
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