[SMT-COMP] SMTCOMP clarification

[David Cok]

SMT-COMP participants:

In earlier email I commented on the bugs exposed during SMT-COMP in CVC4 
and Yices2. These tools, along with veriT, SMTInterpol, and CVC3 entered 
a large number of SMT-COMP divisions (all 34, 15, 17, 8, and 19, 
respectively, of which 26, 15, 17, 8, and 11 were medal-competitive). 
All other entrants entered just 1 or 2 divisions. I should expand on my 
comments.

These bugs were noticed because they resulted in an incorrect answer (we 
don't notice the bugs that give the right answer for wrong reasons). 
However, in neither case are they bugs in the soundness of the 
fundamental algorithms underlying the tools. The authors may wish to 
comment further, but as I understand it:
- CVC4's bug was (one line) in its pre-processing code. It was triggered 
on this particular scrambling of the benchmark, and not on the 
unscrambled benchmark or most other scramblings. It is one of those 
kinds of bugs that every substantial tool has - triggered only on rare 
situations and generally encountered only with significant testing.
- Yices's bug was a buffer overflow that caused the incorrect answer and 
then crashed the tool (which could be a warning not to believe the 
answer); the bug is limited to bitvector problems.  Another benchmark 
encountered the same bug and crashed the tool before giving an answer, 
so that was declared an 'unknown' response.

Tools that apply to many divisions are particularly useful in software 
verification, and I expect in other domains. [We regularly use Yices, 
CVC4, and Z3 currently at GrammaTech]. You should not take from my 
earlier cryptic comments any indication of lack of trust in or lack of 
usefulness in these tools. Quite the contrary actually - I consider them 
well-engineered and highly useful and am appreciative of the substantial 
work that has been invested in them.

- David