diff options
| author |  leino <unknown> | 2015-03-13 02:25:17 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-03-13 02:25:17 -0700 |
| commit | 708970a6d1af5f6d9d28aaafbf0db5972bccf3bc (patch) | |
| tree | 90ee405267404029e3487b2b10d3e64b447e2905 /Test/dafny4/Bug54.dfy | |
| parent | 0b7c479b76c4ebc8ae3cba0cbe0a7cbb0a19144a (diff) | |
| parent | feee322b21fa0d83fd6e86142685f27bc6b73f8b (diff) | |
Merge
Diffstat (limited to 'Test/dafny4/Bug54.dfy')
| -rw-r--r-- | Test/dafny4/Bug54.dfy | 26 |
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 |