diff --git a/Test/civl/samples/snapshot.bpl b/Test/civl/samples/snapshot.bpl index 6b2537661..23d2ac40f 100644 --- 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]; } -} \ No newline at end of file +} + +yield procedure {:layer 0} read_s({:linear} tid: One Tid, i: int); +refines action_read_s;