[SMT-COMP] SMT-COMP 2016: Incorrect Answers (Application Track)

[Tjark Weber]

Christoph,

On Wed, 2016-07-06 at 21:26 +0000, Christoph Wintersteiger wrote:
> Could you give us a quick explanation of what the numbers in the .csv file mean? (Or a pointer if that's been writing up elsewhere?)

Certainly. I downloaded the original CSV files from StarExec, but then
the column headers fell victim to my filtering.

For the main and "unknown benchmarks" tracks:

pair id,benchmark,benchmark id,solver,solver
id,configuration,configuration id,status,cpu time,wallclock time,memory
usage,result,expected

For the application track:

pair id,benchmark,benchmark id,solver,solver
id,configuration,configuration id,status,cpu time,wallclock time,memory
usage,result,wrong-answers,correct-answers

For the unsat-core track:

pair id,benchmark,benchmark id,solver,solver
id,configuration,configuration id,status,cpu time,wallclock time,memory
usage,result,expected,
validation-check-sat-time_cvc4,validation-check-sat-result_z3,
validation-check-sat-time_z3,validation-check-sat-result_mathsat,
unsat-core-validated,result-is-erroneous,parsable-unsat-core,
validation-check-sat-result_cvc4,validation-check-sat-time_mathsat,
size-unsat-core,number-of-assert-commands,check-sat-result-is-erroneous,reduction

IDs are those used by StarExec. For instance, you can look at job pair
221658547 by pointing your browser to
https://www.starexec.org/starexec/secure/details/pair.jsp?id=221658547

Please do not hesitate to ask if you have further questions.

Best,
Tjark