[SMT-COMP] StarExec questions

[Delcypher]

On 12 June 2017 at 16:55, Tjark Weber <tjark.weber at it.uu.se> wrote:
> Dan,
>
> On Mon, 2017-06-12 at 16:48 +0100, Delcypher wrote:
>> Under the "result" column does "starexec-unknown" mean the same thing
>> as the solver responding "unknown"?
>
> Not quite. It depends on the post-processor; if you are using the
> "SMT-COMP 2016" post-processor, the result will be starexec-unknown
> *unless* the solver output contains either sat or unsat (and not both).
> For instance, it could also mean that the solver generated no output at
> all.

Ah okay. Thanks for explaining. Perhaps this information could make
its way into some sort of documentation next year? It would make it
easier for newcomers like me to get started.

Thanks,
Dan.