The benchmark selection program is somewhat different from last year's. It uses the status, difficulty, and category of the benchmarks, but doesn't read them from the benchmark files themselves. Rather, this information is extracted from a MySQL database used for SMT-COMP'07, and a benchmark selection program is run on this extracted metadata to form the final list of selected benchmarks.
The metadata differs from the values encoded in the benchmark files in three ways:
For each division, the check benchmarks are always included. In addition, the selection script will randomly select 100 benchmarks from each division with the following distribution (when possible): 85 industrial, 10 crafted, and 5 random. In each category, the script selects (when possible) 25% easy-sat, 25% easy-unsat, 25% hard-sat, and 25% hard-unsat. A benchmark is easy if it has difficulty 0, 1, or 2. A benchmark is hard if it has difficulty 3, 4, or 5.
If there aren't enough random and crafted, then the slack is “inherited” by the industrial category. It there aren't enough industrial, then the slack is “inherited” by the crafted category.
More detail on this procedure is included in a comment at the top of the source file, and in the rules PDF for this year's competition.
The actual benchmarks selected for competition this year are listed on the selected benchmarks page.