Semantics for "(set-info :status sat/unsat")

[Mikoláš Janota]

Hi 

Is there a differentiation between a problem being SAT and UNSAT because there is a solver that has solved the problem and between the author of the problem believing it has a particular status?

Both the author and the solver can be wrong but we would hope that the chances of the solver being wrong are lower :) Hence the difference.

Cheers

-Mikolas

[Clark Barrett]

We have not made this distinction.  We allow both, but periodically do try to confirm as many as possible by solving with multiple solvers and long time limits.  Thus, it is possible that some difficult problems that no solver can solve might be mislabeled by the author.  So far, this has happened only very rarely.

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/1263dff4-8aff-4ab7-a276-0e1ffb99c372n%40googlegroups.com.