[SMT-COMP] benchmark data

[David Cok]

Per the rules, benchmarks are excluded if all solvers acting on them in 
the SMT-EVAL-2013 run completed in less than 5 seconds. That is what is 
meant in the table by trivial.

We are intending to include all the benchmarks we can, given the 
resources. Our current estimates are that we can't quite do that for the 
divisions with several thousand eligible benchmarks, but we are refining 
our estimates of the average computation time to have a better sense of 
what to expect.  Also, as described in the rules, we will be dividing 
large divisions into heats, and will execute as many heats as possible 
before the end of the competition.

- David

On 6/9/2014 12:05 PM, Bruno Dutertre wrote:
> 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
>