Force write-after-read for AtomicInc nodes

src/pairs/analysis/modules.py

@@ -39,8 +39,16 @@ class FetchModulesReferences(Visitor):
             self.visit(ast_node.capacity)
 
     def visit_AtomicInc(self, ast_node):
+        visit_once = self.visit_nodes_once
+        self.visit_nodes_once = False
+        # Force write after read for the same node (visited twice)
+        self.writing = False
+        self.visit(ast_node.elem)
         self.writing = True
         self.visit(ast_node.elem)
+        self.visit_nodes_once = visit_once
+
+
         self.writing = False
         self.visit(ast_node.value)
 

src/pairs/transformations/expressions.py

@@ -194,18 +194,6 @@ class AddExpressionDeclarations(Mutator):
 
         return ast_node
     
-    def mutate_AtomicInc(self, ast_node):
-        self.writing = True
-        ast_node.elem = self.mutate(ast_node.elem)
-        self.writing = False
-        ast_node.value = self.mutate(ast_node.value)
-        atomic_inc_id = id(ast_node)
-        if atomic_inc_id not in self.declared_exprs and atomic_inc_id not in self.params:
-            self.push_decl(Decl(ast_node.sim, ast_node))
-            self.declared_exprs.append(atomic_inc_id)
-
-        return ast_node
-
     def mutate_Block(self, ast_node):
         block_id = id(ast_node)
         self.decls[block_id] = []