[SMT-COMP] Analysis of Main Track Solver Output With Strict Post-Processing

[Tjark Weber]

The post-processor used to analyze solver output for SMT-COMP 2015
classifies output that it doesn't understand as "unknown" (so that
solvers aren't assigned a wrong answer unless they really produced a
wrong answer).

This approach, while appropriate for SMT-COMP, can mask errors in
solvers.

Independently of the competition (and using a much shorter timeout), I
have analyzed the output of all main track solvers with a stricter
post-processor that flags any output other that "sat", "unsat" or
"unknown" as an error. The results are available here:

  https://www.starexec.org/starexec/secure/details/job.jsp?id=8419

I would encourage solver developers to take a look especially at those
job pairs that are classified as "wrong" to see if their solver
produces unexpected output and/or could be made more SMT-LIB compliant.

I am aware of the limitations of this analysis; there are likely false
positives, and I do not claim that any solver needs to be "fixed." I
simply hope that the data will be helpful to identify some issues in
some solvers.

Once again, this is independent of SMT-COMP, and has no bearing on the
competition results.

Best,
Tjark