[SMTChecker] Support memory/storage pointers

Currently aliasing is "supported" by erasing knowledge about all variables of reference type T when another variable of type T is modified (assignment, push, pop).
This includes subtypes of arrays/mappings, for example.

This issue collects ideas on how to implement better support for those.

Start by reading the SMTChecker implementation and the aliasing behavior described in this issue. Investigate how assignments, push, and pop erase knowledge for reference types, then determine what better memory/storage pointer support should cover. Done requires an agreed approach and implementation scope, since the issue currently collects ideas rather than specifying a change.

Written by the indexing model from the issue text.