diff options
| author |  Jason Koenig <unknown> | 2011-07-14 19:04:48 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-14 19:04:48 -0700 |
| commit | bd0939ffe92812966dfe2aac15d28cc1e3c37b42 (patch) | |
| tree | ea5861dcf473be51b024b7fe178e820e8be18c9d /Test/dafny0/TypeAntecedents.dfy | |
| parent | 5e9cfe9da36b5efda394c1bde3f5536f1a5308a0 (diff) | |
Fixed failing regression tests.
Diffstat (limited to 'Test/dafny0/TypeAntecedents.dfy')
| -rw-r--r-- | Test/dafny0/TypeAntecedents.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index 710e9838..5982a9e6 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -87,8 +87,8 @@ method N() returns (k: MyClass) {
k := new MyClass;
}
-
-function NF(): MyClass
+var a: MyClass;
+function NF(): MyClass reads this; { a }
function TakesADatatype(a: List): int { 12 }
|