[SMT-LIB] bitvector benchmarks

[Clark Barrett]

I have added a preliminary set of bitvector benchmarks to SMT-LIB.  They are
preliminary because:

1) the theory and logic have not been formally approved (though I think they
   are very close)

2) these are only a sample of the final set of benchmarks I plan to post.  I
   haven't had time to translate all of them yet.

Because I am travelling for the next couple of weeks, I expect the final set of
BV benchmarks to be posted by the end of the first week of June.
Unfortunately, this is a little later than we had hoped in our timeline for
SMT-COMP, but it will have to slip a bit.

-Clark