added bug in atomicity analysis

test/bugs/atomicity_check_ghost_field_bug.rav

@@ -0,0 +1,25 @@
+field f1: Int
+ghost field g1: Int
+
+inv inv1() { true }
+
+proc p1(x: Ref) 
+    requires inv1()
+    requires exists nn:Int :: own(x, f1, nn, 1.0)
+{
+    unfold inv1();
+        var f: Int := x.f1;
+
+        // ########
+        // Neither of the following succeed:
+        // a.)
+           x.g1 := 4;
+        // 
+        // b.)
+        //    {! x.g1 := 4; !}
+        // 
+        // for similar reasons.
+        // ########
+
+    fold inv1();
+}