13 files changed, 36 insertions, 23 deletions
diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
index 9535d677..63f5df23 100644
--- a/Test/VSComp2010/runtest.bat
+++ b/Test/VSComp2010/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 
 for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy
             Problem3-FindZero.dfy Problem4-Queens.dfy
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index 611f9251..f5b9d1b9 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 
 for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (
   echo.
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 0da7fe3e..ac7c8aed 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
 
 for %%f in (Simple.dfy) do (
   echo.
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 9ed6d75a..7c7719ee 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -1,8 +1,4 @@
 
--------------------- BQueue.bpl --------------------
-
-Boogie program verifier finished with 8 verified, 0 errors
-
 -------------------- Queue.dfy --------------------
 
 Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 1f5d78df..d098d753 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -3,14 +3,6 @@ setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
-
-for %%f in (BQueue.bpl) do (
-  echo.
-  echo -------------------- %%f --------------------
-  %BPLEXE% %* %%f
-)
 
 for %%f in (Queue.dfy PriorityQueue.dfy
             ExtensibleArray.dfy ExtensibleArrayAuto.dfy
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 93524dfa..9c37549e 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -35,6 +35,10 @@ Dafny program verifier finished with 5 verified, 0 errors
 
 Dafny program verifier finished with 3 verified, 0 errors
 
+-------------------- TuringFactorial.dfy --------------------
+
+Dafny program verifier finished with 3 verified, 0 errors
+
 -------------------- StoreAndRetrieve.dfy --------------------
 
 Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/dafny2/TuringFactorial.dfy b/Test/dafny2/TuringFactorial.dfy
new file mode 100644
index 00000000..585c998e
--- /dev/null
+++ b/Test/dafny2/TuringFactorial.dfy
@@ -0,0 +1,26 @@
+function Factorial(n: nat): nat
+{
+  if n == 0 then 1 else n * Factorial(n-1)
+}
+
+method ComputeFactorial(n: int) returns (u: int)
+  requires 1 <= n;
+  ensures u == Factorial(n);
+{
+  var r := 1;
+  u := 1;
+  while (r < n)  
+    invariant r <= n;
+    invariant u == Factorial(r);
+  { 
+    var v, s := u, 1;
+    while (s < r + 1)
+      invariant s <= r + 1;
+      invariant v == Factorial(r) && u == s * Factorial(r);
+    {
+      u := u + v;
+      s := s + 1;
+    }
+    r := r + 1;
+  }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 794b7908..b68ba251 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 
 REM soon again:    SnapshotableTrees.dfy 
 for %%f in (
@@ -14,7 +13,7 @@ for %%f in (
     COST-verif-comp-2011-2-MaxTree-datatype.dfy
     COST-verif-comp-2011-3-TwoDuplicates.dfy
     COST-verif-comp-2011-4-FloydCycleDetect.dfy
-    Intervals.dfy TreeFill.dfy
+    Intervals.dfy TreeFill.dfy TuringFactorial.dfy
     StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy
   ) do (
   echo.
diff --git a/Test/textbook/Answer b/Test/textbook/Answer
index dace3eb3..42e41c5a 100644
--- a/Test/textbook/Answer
+++ b/Test/textbook/Answer
@@ -22,3 +22,7 @@ Boogie program verifier finished with 1 verified, 0 errors
 ------------------------------ TuringFactorial.bpl ---------------------
 
 Boogie program verifier finished with 1 verified, 0 errors
+
+------------------------------ BQueue.bpl ---------------------
+
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/dafny1/BQueue.bpl b/Test/textbook/BQueue.bpl
index 77f1efb3..77f1efb3 100644
--- a/Test/dafny1/BQueue.bpl
+++ b/Test/textbook/BQueue.bpl
diff --git a/Test/textbook/runtest.bat b/Test/textbook/runtest.bat
index b747312d..f43e54d9 100644
--- a/Test/textbook/runtest.bat
+++ b/Test/textbook/runtest.bat
@@ -7,7 +7,7 @@ REM ======================
 REM ====================== Examples written in Boogie
 REM ======================
 for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl McCarthy-91.bpl
-            TuringFactorial.bpl) do (
+            TuringFactorial.bpl BQueue.bpl) do (
   echo.
   echo ------------------------------ %%f ---------------------
   %BPLEXE% %* %%f
diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
index efe7b3d5..cd047d39 100644
--- a/Test/vacid0/runtest.bat
+++ b/Test/vacid0/runtest.bat
@@ -3,8 +3,6 @@ setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 
 for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (
   echo.
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 770f41dc..7f7c9b9f 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -3,7 +3,6 @@ setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 
 for %%f in (
     Two-Way-Sort.dfy