[SMT-LIB] Bitvector language in SMTLIB

[Vijay Ganesh]

Dear Friends,

I would like to make some suggestions with regard to the SMTLIB bitvector
language.

* It would be nice to allow constants expressed in binary and hexadecimal
format. Currently, the language supports only decimal format for
constants. Hence, we are forced to put an extraction operator on top of
the decimally-represented constant in order to know its length.
Binary/Hexadecimal formats will obviate the need for extractions over
constants.

* Limiting the language to BV(32) is, well, too limiting. It would be
great if we could allow fixed-length variables/constants of any length.
There are many applications which require vectors of 64 bits or more.
Furthermore, it allows us to effectively parameterize the input, and thus
stress test our systems and know their limits.

* Support for DIV/MOD (signed and unsigned)

Thanks for your time,
Vijay Ganesh