1 files changed, 65 insertions, 0 deletions
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
new file mode 100644
index 00000000..f79f8fb5
--- /dev/null
+++ b/Test/linear/typecheck.bpl
@@ -0,0 +1,65 @@
+type X;
+
+procedure A()
+{
+    var {:linear "A"} a: X;
+    var {:linear "A"} b: int;
+}
+
+procedure B()
+{
+    var {:linear "B"} a: X;
+    var {:linear "B"} b: [X]bool;
+}
+
+procedure C()
+{
+    var {:linear "C"} a: X;
+    var {:linear "C"} c: [X]int;
+}
+
+function f(X): X;
+
+procedure D()
+{
+    var {:linear "D"} a: X;
+    var {:linear "D"} x: X;
+    var {:linear "D"} b: [X]bool;
+    var c: X;
+    var {:linear "D2"} d: X;
+
+    b[a] := true;
+
+    a := f(a);
+
+    a := c;
+
+    c := a;
+
+    a := d;
+
+    a := a;
+
+    a, x := x, a;
+
+    a, x := x, x;
+
+    call a, x := E(a, x);
+
+    call a, x := E(a, a);
+
+    call a, x := E(a, f(a));
+
+    call a, x := E(a, d);
+
+    call d, x := E(a, x);
+
+    call a, x := E(c, x);
+
+    call c, x := E(a, x);
+}
+
+procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
+{
+    c := a;
+}
+\ No newline at end of file