diff options
author | rustanleino <unknown> | 2010-06-08 20:09:12 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2010-06-08 20:09:12 +0000 |
commit | bcd8949ab6d5bd86dc3e81226b1f936d05babfa4 (patch) | |
tree | d2ea8016b651c53840cc9928fd5958a06109d004 /Test/dafny1/Celebrity.dfy | |
parent | b33ec85f6a0bf52f767dc98d9d51e3eab8d51226 (diff) |
Dafny: Fix type bug in SplitExpr translation.
Diffstat (limited to 'Test/dafny1/Celebrity.dfy')
-rw-r--r-- | Test/dafny1/Celebrity.dfy | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index fd267c71..eed06bb1 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -72,8 +72,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)
requires 0 < n;
requires (forall p :: p in people <==> 0 <= p && p < n);
- // requires IsCelebrity(c, people); // see next line:
- requires c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)); // hack to work around bug in Dafny-to-Boogie translator
+ requires IsCelebrity(c, people);
ensures r == c;
{
r := 0;
|