[SMT-COMP] SMT-COMP 2016: Main Track Test Job

Tjark Weber tjark.weber at it.uu.se
Fri May 27 10:27:20 EDT 2016


Christoph,

On Fri, 2016-05-27 at 13:37 +0000, Christoph Wintersteiger wrote:
> Could you explain what the result "starexec-unknown" means?

This is simply the StarExec encoding for when the solver answers
"unknown". (Note that "unknown" is defined by SMT-LIB, while StarExec
is a much more general cross-community service.)

StarExec needs to treat this situation specially because answering
"unknown" is not incorrect even when the expected result for a
benchmark is "sat" or "unsat", i.e., different from "unknown".

Best,
Tjark




More information about the SMT-COMP mailing list