1 files changed, 26 insertions, 0 deletions
diff --git a/Test/dafny4/Bug54.dfy b/Test/dafny4/Bug54.dfy
new file mode 100644
index 00000000..c975ec9a
--- /dev/null
+++ b/Test/dafny4/Bug54.dfy
@@ -0,0 +1,26 @@
+// RUN: %dafny /compile:0  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate G<X>(f:X->bool)
+  reads f.reads;
+  requires forall x :: f.requires(x) && f(x);
+{
+  true
+}
+
+predicate H()
+{
+  G((x:int) => true)
+}
+
+predicate P1<X>(m:map<X,bool>)
+  requires forall x :: x in m ==> m[x];
+{
+  true
+}
+
+predicate P2(m:map<int,bool>)
+  requires forall x :: x in m ==> m[x];
+{
+  P1(map x:int | x in m :: true)
+}
+\ No newline at end of file