Test/dafny4/Bug55.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14

// RUN: %dafny /compile:0  "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

predicate {:opaque} G(f:int->bool)
  reads f.reads;
  requires f.requires(0);
{
  true
}

predicate A<T>(s:set<T>)

predicate{:opaque} B(s:set<int>)
    requires A(s);