[SMTCOMP] degree of difficulty in QF_UFBV[32]

[Leonardo de Moura]

Hi all,

As you probably know, the SMT-COMP website describes the
approach used to compute how "difficult" a benchmark is.
(http://www.csl.sri.com/users/demoura/smt-comp/bench_selection.shtml).
However, we used a different approach for QF_UFBV[32],
because none of the solvers listed on the website supported
the bitvector theory and/or a parser for the new SMT-LIB
extensions. Our first idea was to assign degree 5 to everything, but
this would be bad because there are several easy benchmarks, and
we could end with a trivial division.

So, we decided to use a recent version of CVC Lite to
compute the difficulty levels. The degree of difficulty
was obtained using the following table:

Time         Lvl
0             :     0
< 5          :     1
< 10        :    2
< 100     :     3
< 1000   :    4
timeout  :    5

Note this is not nepotism. This alternative approach does *not* give
an advantage to CVC Lite. Actually, it is bad for CVC Lite
because half of the benchmarks selected for SMT-COMP will
be hard for CVC Lite.

Leonardo