From 47c23bd0d7e71722a94b8df660c0314381b4263a Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Fri, 15 Jul 2011 17:42:55 -0700
Subject: Fixed regression test failures due to removal of bodiless methods and
 functions.

---
 Test/VSI-Benchmarks/Answer      | 12 ------------
 Test/VSI-Benchmarks/runtest.bat |  4 +++-
 2 files changed, 3 insertions(+), 13 deletions(-)

(limited to 'Test/VSI-Benchmarks')

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 2a4587f4..e2456408 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -7,10 +7,6 @@ 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
@@ -22,11 +18,3 @@ 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 a733a1c0..799e1d40 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -6,7 +6,9 @@ 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 (
+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 (
   echo.
   echo -------------------- %%f --------------------
 
-- 
cgit v1.2.3