[Analyses integer sets instead of signed words in NuSMV
Currently an integer is converted to a signed word in NuSMV. Word arithmetic is different than integer one. If a variable v is incremented at every tick, and has a bound = max_word, then it will never go out of bound when using signed words, but will go out of bound if using integers.
Moreover, the number of bits is more of a platform issue and should not be affecting analyses at this level of abstraction.
This could make model checker run slower, so investigation is needed first. In case it makes model checker run too slow, other solution is to be devised.
(from redmine: issue id 2714, created on 2016-10-12, closed on 2016-11-07)