summaryrefslogtreecommitdiff
path: root/Test/linear/typecheck.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/linear/typecheck.bpl')
-rw-r--r--Test/linear/typecheck.bpl4
1 files changed, 3 insertions, 1 deletions
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index 57080cb8..5c936dd0 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -65,9 +65,11 @@ procedure {:yields} {:layer 1} D()
yield;
}
-procedure E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
+procedure {:yields} {:layer 1} E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
{
+ yield;
c := a;
+ yield;
}
procedure {:yields} {:layer 0} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X);