1 files changed, 24 insertions, 0 deletions
diff --git a/Test/test21/Coercions2.bpl b/Test/test21/Coercions2.bpl
new file mode 100644
index 00000000..c5abb724
--- /dev/null
+++ b/Test/test21/Coercions2.bpl
@@ -0,0 +1,24 @@
+
+
+type Box, C;
+
+function box<a>(a) returns (Box);
+function unbox<a>(Box) returns (a);
+
+axiom (forall<a> x:a :: unbox(box(x)) == x);
+
+axiom (forall<a> x:Box :: {unbox(x):a} box(unbox(x):a) == x);
+
+axiom (forall x:Box :: box(unbox(x)) == x);     // warning
+
+procedure P() {
+  var b : Box;
+  var i : C;
+
+  assert unbox(box(13)) == 13;
+
+  i := unbox(b);
+  assert b == box(i);
+
+  assert false;
+}
+\ No newline at end of file