blob: bcbef2e852610f9e230e8184d6f6db8433d859a5 (
plain)
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);
|