[SMT-COMP] benchmark data

[Bruno Dutertre]

On 06/09/2014 07:27 AM, David Cok wrote:
> SMTCOMP competitors:
>
> The current data on benchmarks for SMT-COMP 2014 has been posted to
> http://smtcomp.sourceforge.net/2014/difficulties.shtml
> Note the caveats about this data - we are still correcting errors in the benchmarks, running trial runs to determine difficulty ratings, and trial runs to determine sat/unsat status of (some of the) currently unknown benchmarks. When benchmarks are updated the benchmark ids change - to be using current benchmarks, you need to recopy benchmarks into your trial spaces.
>
> Thanks for email pointing out mal-formed benchmarks. Those are being corrected, primarily by Clark Barrett and Morgan Deters. Let us know of others you find.
>
> Our initial capacity estimates indicate that for most of the divisions, we will be able to run all of the eligible benchmarks (those that are non-trivial and have a known status).
> (With the reorganization of benchmarks, there are now many divisions with <1000 benchmarks).
>

What's the definition of non-trivial? This seems highly subjective.
If trivial implies easy, and you have enough resources, I don't see why
you don't just include all the benchmarks with a known status.

Bruno