encoding.integers is rarely usable

[ThomasHaas]

Some PR (probably the LLVM rework?) removed the ability to parse a program as integers and instead moved all integer reasoning to the encoder (when encoding.integers=true). This does not work well in practice because for integer encoding to be usable, we need to rewrite bitwise operators. In particular, many xor operators (for boolean negation) are generated by LLVM even if the original source does not have bit-vectors operations.

We used to have this rewriting in the parsers for Boogie and LLVM (I think I implemented this twice).
We should introduce a pass that does this rewriting at the very end when using integer encoding.