From f48f5e1cef6482557d3f90677c5e41b75b2092b4 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 1 Mar 2016 16:24:26 -0800
Subject: Added test case to go with the recent fix of Issue #49 (changeset
 f354709009a5).

---
 Test/dafny4/Bug49.dfy        | 74 ++++++++++++++++++++++++++++++++++++++++++++
 Test/dafny4/Bug49.dfy.expect |  8 +++++
 2 files changed, 82 insertions(+)
 create mode 100644 Test/dafny4/Bug49.dfy
 create mode 100644 Test/dafny4/Bug49.dfy.expect

diff --git a/Test/dafny4/Bug49.dfy b/Test/dafny4/Bug49.dfy
new file mode 100644
index 00000000..887938d6
--- /dev/null
+++ b/Test/dafny4/Bug49.dfy
@@ -0,0 +1,74 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main()
+{
+  print apply(i => i + 1, 5), "\n";
+  print mapply(map[5 := 6], 5), "\n";
+  var f;
+  print five(f), "\n";
+}
+
+// -----
+// test that the definition axiom for function "apply" is available
+
+function method apply(f:int->int, a:int): int
+  reads f.reads
+  requires f.requires(a)
+{
+  f(a)
+}
+
+lemma TestPost()
+  ensures apply(i => i + 1, 5) == 6
+{
+}
+
+lemma M() {
+  assert apply(i => i + 1, 5) == 6;
+}
+
+lemma TestPre()
+  requires apply(i => i + 1, 5) == 6
+{
+}
+
+lemma TestPreCaller()
+{
+  TestPre();
+}
+
+// -----
+// test that the above thing for arrows also works for maps
+
+function method mapply(m: map<int,int>, a:int): int
+  requires a in m
+{
+  m[a]
+}
+
+lemma TestMPost()
+  ensures mapply(map[5 := 6], 5) == 6
+{
+}
+
+lemma N() {
+  assert mapply(map[5 := 6], 5) == 6;
+}
+
+// -----
+// test that g's result is known to be $Is'ed and $IsAlloc'ed
+
+function method five(f:int->int): int { 5 }
+
+lemma P() {
+  var f := i => i + 1;
+  assert five(f) == 5;
+}
+
+lemma Q(g: real->int->int)
+  requires g.requires(0.0)
+{
+  var f := g(0.0);
+  assert five(f) == 5;
+}
diff --git a/Test/dafny4/Bug49.dfy.expect b/Test/dafny4/Bug49.dfy.expect
new file mode 100644
index 00000000..653dda07
--- /dev/null
+++ b/Test/dafny4/Bug49.dfy.expect
@@ -0,0 +1,8 @@
+
+Dafny program verifier finished with 21 verified, 0 errors
+Program compiled successfully
+Running...
+
+6
+6
+5
-- 
cgit v1.2.3