Make atomic load and store of pointers work. Tighten verification of atomic operations