diff options
| author |  Shaz Qadeer <qadeer@microsoft.com> | 2015-10-26 21:12:35 -0700 |
|---|---|---|
| committer | Shaz Qadeer <qadeer@microsoft.com> | 2015-10-26 21:12:35 -0700 |
| commit | e037ca99cdc163ca43690aaef3c380ebc1ce1962 (patch) | |
| tree | ad700cd6874eab589f87f2915a9aee1d49d96b50 /Test | |
| parent | deef37064f673be0391a7224ed8551b1e68be829 (diff) | |
fixed
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/linear/typecheck.bpl | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index b4f784d3..c3c294c9 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -89,11 +89,14 @@ modifies g; procedure {:yields} {:layer 0} I({:linear_in ""} x:int) returns({:linear ""} x':int) { + yield; x' := x; + yield; } procedure {:yields} {:layer 0} J() { + yield; } procedure {:yields} {:layer 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int) |