[SMT-COMP] SMTCOMP clarification
David Cok
dcok at grammatech.com
Sun Jun 22 09:00:15 EDT 2014
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
More information about the SMT-COMP
mailing list