[SMTCOMP] final rules posted

[Aaron Stump]

This is just to announce that we have revised the SMT-COMP 2006 rules
according to the community feedback we received.  Thanks to all who
gave us suggestions on this.  The rules are posted on the SMT-COMP 2006
site:

http://www.csl.sri.com/users/demoura/smt-comp/

Below is copied a summary of the suggestions we received ("--") and our
responses ("**").

Best wishes,
Aaron
for Clark and Leonardo, too.
----------------------------------------------------------------------
Windows
   
   -- could we also support Windows in addition to linux.

   ** no, we should not try to support Windows.  Running the competition
      on multiple platforms is likely to provoke criticism, and isn't it
      the case that for remote execution machines need to be running
      Remote Desktop Server?

Other results

   -- Results reported to the organizers by tools in a demonstration
      division should not be reported unverified to the public.

   ** well, that is a point.  We are dropping the "demonstration
      division".

Benchmarks

   -- Make *all* benchmarks available in advance

   ** yes, we should definitely do this, and not spring any 
      new benchmarks on people that they haven't had a chance to run.
   
Scrambling

   -- do perform simple formula scrambling.
   -- do not scramble structure; also there may be no point because
      simple scrambling can be easily defeated by an adversary

   ** we will design a simple pseudo-random scrambler, and publish it
      enough in advance so that people can make sure their tools handle
      its output.
      
Buggy solvers: 

   -- do eliminate solvers with more than some number of bugs.

   -- either disqualify solvers with even one buggy answer, or else
      just use the point system to penalize them out of contention.
      The compromise we suggest is hard to justify.

   ** We respectfully disagree with the last point, and will stick with
      the proposed scheme (disqualify a tool from all divisions if in
      any one division it gets more than three wrong answers; penalize
      by 8 points for each wrong answer).

Benchmark selection

   -- do allow secret benchmarks
   -- uniformly random selection will be biased if the set of
      benchmarks contain a disproportionate number of benchmarks
      of a particular kind (e.g., "synthetic") 

   ** no secret benchmarks, although it would be an intriguing twist to
      the competition; also, we must try to avoid skewing the selection
      to one kind of benchmark, as much as possible.

Community building

   -- organize an informal dinner at FLoC.

   ** sounds good. 

Bitvectors

   -- the theory will probably be specified by end of March 

Quantifiers

   -- try to add a division with quantified formulas 

   ** ok, if we have some formulas (as it sounds like we will).