Comments: Proposal for a theory of fixed-size bit-vectors in SMT-LIB format

[Leonardo de Moura]

Hi Silvio and Cesare,

I'm still having problems with my QPQ account. So, I'm sending my
comments direct to you.

- Use bvadd, bvsub, bvuminus, bvmul, bvle, bvge, bvlt, bvgt instead of
   +, -, *, <=, >=, <, >.

- Use overloading only for "theory" functions and predicates. I mean,
one should not be able to overload uninterpreted functions/predicates.

- I think it would be nice to include bv2nat and nat2bv.  For instance,
nat2bv is useful for specifying bitvector constants. I guess nat2bv
needs to be indexed with the size of the resulting bitvector.

Cheers,
Leonardo.