summaryrefslogtreecommitdiff
path: root/Test/test21/Casts.bpl
diff options
context:
space:
mode:
authorGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
committerGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
commitce1c2de044c91624370411e23acab13b0381949b (patch)
tree592539996fe08050ead5ee210c973801611dde40 /Test/test21/Casts.bpl
Initial set of files.
Diffstat (limited to 'Test/test21/Casts.bpl')
-rw-r--r--Test/test21/Casts.bpl11
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