Add new memory model

Encodes pointers symbolically and does points-to analysis