Checking results and outputs: What makes a solver Buggy

Let us notice a tricky consideration about buggy solvers. If SAT was claimed on a satisfiable instance, but the certificate was not correct, then unknown (and not buggy) was assumed as an answer. Each SAT result is thus certified, and we did not consider as buggy a solver that gave a wrong certificate (this can be due for instance to a CPUs exceed while printing the certificate or to a data structure problem if the certificate is displayed on a single line). As a matter of fact, we only considered as ``buggy'' all solvers that answered incorrectly, UNSAT on a SAT instance (previously known SAT or proved by any other solver during the competition). In addition, solvers are by essence incomplete, because of memory and CPU limitation. Thus, if a solver crashed during the competition (which can be due or not to bugs), we did not consider it as buggy. We only considered that its answer was ``unknown''.

Each time a buggy solver was found, it was tagged hors-concours and discarded from the awards (results were still available ``unofficially'').