summaryrefslogtreecommitdiff
path: root/Test/og/one.bpl
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-11-14 22:18:15 -0800
committerGravatar qadeer <unknown>2014-11-14 22:18:15 -0800
commit72d74c23e9c5cc1903f2646af6a7d778cfde53f3 (patch)
tree42b738427237ff44692051f028fb92a427c3cd1b /Test/og/one.bpl
parent0339351e985c455e7ecf290be54aa5361fe7ae8f (diff)
renamed :phase to :layer
Diffstat (limited to 'Test/og/one.bpl')
-rw-r--r--Test/og/one.bpl8
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 2da898d6..45cbbda3 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,18 +1,18 @@
// RUN: %boogie -noinfer "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-var {:phase 1} x:int;
+var {:layer 1} x:int;
-procedure {:yields} {:phase 0,1} Set(v: int);
+procedure {:yields} {:layer 0,1} Set(v: int);
ensures {:atomic}
|{A:
x := v; return true;
}|;
-procedure {:yields} {:phase 1} B()
+procedure {:yields} {:layer 1} B()
{
yield;
call Set(5);
yield;
- assert {:phase 1} x == 5;
+ assert {:layer 1} x == 5;
}