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 epfl-lara/ScalaZ3#73.

[0] Z3Prover/z3#1481 (comment)
[1] cvc5/cvc5#750

/cc @samarion @jad-hamza @vkuncak