6 files changed, 31 insertions, 38 deletions
diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index e2456408..2a4587f4 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -7,6 +7,10 @@ Dafny program verifier finished with 10 verified, 0 errors
 
 Dafny program verifier finished with 6 verified, 0 errors
 
+-------------------- b3.dfy --------------------
+
+Dafny program verifier finished with 10 verified, 0 errors
+
 -------------------- b4.dfy --------------------
 
 Dafny program verifier finished with 11 verified, 0 errors
@@ -18,3 +22,11 @@ Dafny program verifier finished with 22 verified, 0 errors
 -------------------- b6.dfy --------------------
 
 Dafny program verifier finished with 21 verified, 0 errors
+
+-------------------- b7.dfy --------------------
+
+Dafny program verifier finished with 23 verified, 0 errors
+
+-------------------- b8.dfy --------------------
+
+Dafny program verifier finished with 42 verified, 0 errors
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index 799e1d40..a733a1c0 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -6,9 +6,7 @@ set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
 set BPLEXE=%BOOGIEDIR%\Boogie.exe
 set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 
-REM b3, b7 and b8 need reworking to not use body-less functions and methods.
-
-for %%f in (b1.dfy b2.dfy b4.dfy b5.dfy b6.dfy) do (
+for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (
   echo.
   echo -------------------- %%f --------------------
 
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 5bb746d8..5ee9f921 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -85,12 +85,12 @@ Dafny program verifier finished with 29 verified, 0 errors
 
 -------------------- Rippling.dfy --------------------
 
-Dafny program verifier finished with 122 verified, 0 errors
+Dafny program verifier finished with 132 verified, 0 errors
 
 -------------------- Celebrity.dfy --------------------
 
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
 
 -------------------- UltraFilter.dfy --------------------
 
-Dafny program verifier finished with 20 verified, 0 errors
+Dafny program verifier finished with 19 verified, 0 errors
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index a10c4324..21b895aa 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,26 +1,15 @@
 // Celebrity example, inspired by the Rodin tutorial
 
-class Person
-{
-
-}
-
-var pa: seq<Person>;
-
-function method Knows(a: Person, b: Person): bool
-  reads this;
+static function method Knows<Person>(a: Person, b: Person): bool
   requires a != b;  // forbid asking about the reflexive case
-{
-   exists i | 0 <= i && i < |pa| :: 0 <= i < |pa| / 2 ==> pa[2*i] == a && pa[2*i+1] == b
-}
-function IsCelebrity(c: Person, people: set<Person>): bool
-  reads this;
+
+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
 {
   c in people &&
   (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
 }
 
-method FindCelebrity0(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
   requires (exists c :: IsCelebrity(c, people));
   ensures r == c;
 {
@@ -28,7 +17,7 @@ method FindCelebrity0(people: set<Person>, ghost c: Person) returns (r: Person)
   r := cc;
 }
 
-method FindCelebrity1(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
   requires IsCelebrity(c, people);
   ensures r == c;
 {
@@ -51,7 +40,7 @@ method FindCelebrity1(people: set<Person>, ghost c: Person) returns (r: Person)
   r := x;
 }
 
-method FindCelebrity2(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
   requires IsCelebrity(c, people);
   ensures r == c;
 {
@@ -75,7 +64,7 @@ method FindCelebrity2(people: set<Person>, ghost c: Person) returns (r: Person)
   }
   r := b;
 }
-/*
+
 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);
@@ -99,4 +88,3 @@ method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)
   }
   r := b;
 }
-*/
-\ No newline at end of file
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 78905b6e..0a4d541d 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -157,14 +157,13 @@ function last(xs: List): Nat
     case Cons(z, zs) => last(ys)
 }
 
-/*
 function mapF(xs: List): List
 {
   match xs
   case Nil => Nil
   case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))
 }
-function HardcodedUninterpretedFunction(n: Nat): Nat*/
+function HardcodedUninterpretedFunction(n: Nat): Nat
 
 function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List
 {
@@ -187,7 +186,7 @@ function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List
     else Cons(y, ys)
 }
 
-/*function filterP(xs: List): List
+function filterP(xs: List): List
 {
   match xs
   case Nil => Nil
@@ -196,7 +195,7 @@ function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List
     then Cons(y, filterP(ys))
     else filterP(ys)
 }
-function HardcodedUninterpretedPredicate(n: Nat): Bool*/
+function HardcodedUninterpretedPredicate(n: Nat): Bool
 
 function insort(n: Nat, xs: List): List
 {
@@ -328,22 +327,21 @@ ghost method P11()
 {
 }
 
-/*
 ghost method P12()
   ensures (forall n, xs :: drop(n, mapF(xs)) == mapF(drop(n, xs)));
 {
-}*/
+}
 
 ghost method P13()
   ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs));
 {
 }
-/*
+
 ghost method P14()
   ensures (forall xs, ys :: filterP(concat(xs, ys)) == concat(filterP(xs), filterP(ys)));
 {
 }
-*/
+
 ghost method P15()
   ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs)));
 {
@@ -480,12 +478,12 @@ ghost method P40()
   ensures (forall xs :: take(Zero, xs) == Nil);
 {
 }
-/*
+
 ghost method P41()
   ensures (forall n, xs :: take(n, mapF(xs)) == mapF(take(n, xs)));
 {
 }
-*/
+
 ghost method P42()
   ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs)));
 {
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 0dfb6683..c8419890 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -31,9 +31,6 @@ class UltraFilter<G> {
   // Dafny currently does not have a set comprehension expression, so this method stub will have to do
   method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)
     ensures (forall X :: X in h <==> M + X in f);
-  {
-    assume false;
-  }
 
   method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
     requires IsFilter(f, S);