[tedks]

This is the project webpage, though I can't recall if it uses Z3 or not: http://research.microsoft.com/en-us/projects/slam/

[frik]

Thanks. From that page:

  Pointers in SLAM2: Efficient evaluation of pointer 
  predicates with Z3 SMT Solver in SLAM2