diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-04 11:24:35 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-04 11:24:35 -0700 |
| commit | 47d88acd5e49ea9f68dd93bc2eb8dca85036b7ca (patch) | |
| tree | ae9fe1fd8987d740c38c4989aa91957257d60d3b /Test/og/akash.bpl | |
| parent | 4024e730fe78f4f210b497041ca083b1464426b5 (diff) | |
fixed bug reported by Akash
Diffstat (limited to 'Test/og/akash.bpl')
| -rw-r--r-- | Test/og/akash.bpl | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl index dca4f5f7..fbc97d59 100644 --- a/Test/og/akash.bpl +++ b/Test/og/akash.bpl @@ -39,6 +39,10 @@ requires x_in != mapconstbool(false); assume x_in == x;
g := 1;
+
+ yield;
+
+ g := 2;
}
procedure C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool)
@@ -50,4 +54,8 @@ requires y_in != mapconstbool(false); assume y_in == y;
h := 1;
+
+ yield;
+
+ h := 2;
}
\ No newline at end of file |