fixed order of proc and action

boogie-org · Apr 26, 2024 · ab86f48 · ab86f48
1 parent f5c7a8a
commit ab86f48
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/Test/civl/samples/snapshot.bpl b/Test/civl/samples/snapshot.bpl
@@ -80,9 +80,6 @@ modifies mem;
     mem[i] := StampedValue(x->ts + 1, v);
 }
 
-yield procedure {:layer 0} read_f ({:linear} tid: One Tid, i: int);
-refines action_read_f;
-
 right action {:layer 1} action_read_f ({:linear} tid: One Tid, i: int) 
 modifies r1;
 {
@@ -97,8 +94,8 @@ modifies r1;
     }
 }
 
-yield procedure {:layer 0} read_s({:linear} tid: One Tid, i: int);
-refines action_read_s;
+yield procedure {:layer 0} read_f ({:linear} tid: One Tid, i: int);
+refines action_read_f;
 
 left action {:layer 1} action_read_s({:linear} tid: One Tid, i: int)
 modifies r2;
@@ -113,4 +110,7 @@ modifies r2;
     } else {
         r2[tid->val][i] := mem[i];
     }
-}
+}
+
+yield procedure {:layer 0} read_s({:linear} tid: One Tid, i: int);
+refines action_read_s;