Z3: Investigate switching to BitVec representation

[ana-pantilie]

We need to see if Z3 provides better bitwise reasoning when using the BitVec representation. There is also the question of whether if it's feasible to switch to this, so we need to test performance first. The person investigating this should talk to someone working on KEVM to figure out how to test this.

[ehildenb]

Really what we need to do is this:

• Change the underlying theory we use for Z3 (in our prelude) to be one that includes new bitvectors.
• Change Int operations in domains.md to use smt-hook(bitvec_op) instead of smt-hook(int-op). https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md#integer-arithmetic

For example: