Improve Bit-vector Scalability

[michael-emmi]

(from Shaobo)

There is obviously a scalability issue of SMACK when it is applied on DeviceDriver64 category of SVCOMP benchmarks that requires reasoning about bit-vectors. I think it would be good to improve our support for bit-vectors in order to fix this issue.

I manually inspected some benchmarks[1] and it seems that the number of variables requiring bit-vectors is limited (mainly flags[2]). So I think maybe a dependence analysis could allow us to use bit-vector on these variables while model others as integers though interprocedural support and pointer aliasing could be a big problem. Moreover, Akash's paper, Powering the Static Driver Verifier using Corral also provides a very reasonable solution. I remember you have tried it while it might not work well.