Try Bitwise

[laurentder]

PR to have a first test with the current implementation of integer representations in BitsVector form.
Do not merge with the master for the moment ;-)

Fixes #743

[jhjourdan]

Some notes about this work:

• It would be probably necessary to have an option to opt-in this.
• Try to use mathematical bounded integers and convert them to BV instead of doing the convert
• Should we use type invariants to bound machine integers (then it is easy to have arithmetics on machine integeres in pearlite)