1 files changed, 11 insertions, 0 deletions
diff --git a/Test/test21/Casts.bpl b/Test/test21/Casts.bpl
new file mode 100644
index 00000000..5173021e
--- /dev/null
+++ b/Test/test21/Casts.bpl
@@ -0,0 +1,11 @@
+
+
+procedure P() returns () {
+  var m : [int]int, n : [int]int, x : int;
+
+  assume m[x] == x;
+  assume n[x] == 1;
+
+  assert n[m[x]] == 1;
+  assert m[n[x]] == 1;    // should not be provable
+}
+\ No newline at end of file