[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