Limit Z3 expressions to QF_BV

[senier]

We are currently using unbounded integers when creating Z3 expressions, even though our problem is expressible in the quantifier-free bitvector logiv (QF_BV). This most likely causes a significant performance drop, as Z3 does not invoke the simplex possible solving strategies. Change the Z3 expression such that only bit-vector integers are used and explicitly limit the logic by using SolverFor.

[senier]

This has not resulted in significant performance improvements in our experiments with the fuzzer and overflows need to be handled explicitly which turned out to be complicated. We limit the logic to QF_LIA already which gave a slight performance improvement.