BitVector <-> Integer conversions

[romac]

Since both Z3 [0] and CVC4 [1] apparently support interpreted conversions between bit vectors and integers (via bv2int, int2bv and bv2nat, nat2bv respectively), perhaps we could add support for such conversions in Inox, with a fallback for other solvers via recursive conversion procedures implemented as a theory encoder?

I have a PR for ScalaZ3 with a test for such Int<->BigInt conversions at https://github.com/epfl-lara/ScalaZ3/pull/73.

[0] https://github.com/Z3Prover/z3/issues/1481#issuecomment-365030093 [1] https://github.com/CVC4/CVC4/issues/750

/cc @samarion @jad-hamza @vkuncak