[SMT-LIB] BitVectors32: DIV and MOD

[Vijay Ganesh]

Hi All,

I have the following question regarding signed DIV and MOD. I hope that 
the logic designers can answer it at the earliest.

1. It looks like these operators will be present in the future version of 
the logic. But there are many different standards for defining the 
semantics of these two operators, e.g. Euclidean definition, C99 etc. 
However, for better or worse the most widely accepted standard in 
programming languages is the C99 standard. Since a large number of 
benchmarks come from software applications, I believe it is a good idea to 
use the C99 definitions. Other definitions can be easily encoded in terms 
of the C99 definitions and other bitvector operations.

The question is "Has a decision been made with regard to which definition 
will be used?"

2. I also believe that it is not ok to limit the sorts to a maximum of 32 
bit-vectors. We should allow any number of bits.

Thanks for your time,
Vijay.