The former realization of bv used a bit of sign as the less significant
bit which should be the most significant. It did not raise problems
because to_int and to_uint were not linked by an axiom in the .why. Now,
it is the case, so we rewrote function twos_complement and made some
straightforward changes to the existing realization (surprisingly proofs
are the same).