[SMT-COMP] 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