Improving bitvector solving using tactics

[zvonimir]

It is I guess well-known that Z3 does not do super well when bitvectors are mixed with arrays/functions/quantifiers. Hence, different tactics can be used to first compile away everything into a pure bitvector formula, which is then solved using a faster SAT solver. There is a good discussion here: https://github.com/Z3Prover/z3/issues/577 It would be great to try out these (and similar) tactics on our problems as well. We are certainly doing poorly on anything that involves bitvectors.