[SMT-COMP] SMTCOMP 2018 rules

[Mohamed Iguernlala]

Hello community,

I just realized that the rules for SMTCOMP 2018 were (already)
published[1]. I found the additional evaluation criteria in page
3 really interesting. I wanted to suggest an additional criterion
for the main track (for 2019, if it's too late for 2018).
Evaluate solvers performances:

- on UNSAT answers only, by ignoring all benchmarks with SAT
   status. Of course a solver should not answer UNSAT on a script
   with a SAT status,

- on SAT answers only, by ignoring all benchmarks with UNSAT
   status

In both situations, benchmarks with "unknown" status can either
be kept or ignored.

By the way, I'll probably participate with Ctrl-Ergo[2] in QF_LIA
and QF_LRA.

Best regards,

- Mohamed Iguernlala.

[1] http://smtcomp.sourceforge.net/2018/rules18.pdf
[2] https://gitlab.com/OCamlPro-Iguernlala/Ctrl-Ergo


---
Senior R&D Engineer @ OCamlPro
Research Associate, VALS team, LRI
LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979