Speed up symbolic pointer handling

[vitalych]

Currently, dereferencing a symbolic pointer will send a 4k page to the solver, which is hard on the solver. There is some code that splits 4k pages into smaller chunks, but it currently doesn't work.

https://mail.google.com/mail/u/0/h/1nc2k450m97nh/?&th=17b3cb83c93e80c3&q=s2e-dev&v=c&s=q

Page splitting is a hack though, and it is also hard to implement. See if there are ways to rewrite such queries to make them faster. Solver knowledge would be important here.