From 11e2d2b6d6a8cb6da6d98bc8f102d8375fca26f5 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 5 Jul 2013 17:19:48 -0700
Subject: Added an option to verify each input file separately.

---
 Test/snapshots/Answer      | 8 --------
 Test/snapshots/runtest.bat | 7 ++-----
 2 files changed, 2 insertions(+), 13 deletions(-)

(limited to 'Test/snapshots')

diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
index 676f0323..dc0ee8c1 100644
--- a/Test/snapshots/Answer
+++ b/Test/snapshots/Answer
@@ -1,5 +1,3 @@
-
--------------------- Snapshots0 --------------------
 Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
 Execution trace:
     Snapshots0.v0.bpl(41,5): anon0
@@ -27,8 +25,6 @@ Execution trace:
     Snapshots0.v0.bpl(41,5): anon0
 
 Boogie program verifier finished with 2 verified, 1 error
-
--------------------- Snapshots1 --------------------
 Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
 Execution trace:
     Snapshots1.v0.bpl(13,5): anon0
@@ -46,8 +42,6 @@ Execution trace:
 
 Boogie program verifier finished with 1 verified, 1 error
 
--------------------- Snapshots2 --------------------
-
 Boogie program verifier finished with 1 verified, 0 errors
 
 Boogie program verifier finished with 1 verified, 0 errors
@@ -60,8 +54,6 @@ Boogie program verifier finished with 1 verified, 0 errors
 
 Boogie program verifier finished with 1 verified, 0 errors
 
--------------------- Snapshots3 --------------------
-
 Boogie program verifier finished with 1 verified, 0 errors
 Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.
 Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold.
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat
index 663cef07..e54a19bc 100644
--- a/Test/snapshots/runtest.bat
+++ b/Test/snapshots/runtest.bat
@@ -4,8 +4,5 @@ setlocal
 set BOOGIEDIR=..\..\Binaries
 set BGEXE=%BOOGIEDIR%\Boogie.exe
 
-for %%f in (Snapshots0 Snapshots1 Snapshots2 Snapshots3) do (
-  echo.
-  echo -------------------- %%f --------------------
-  %BGEXE% %* /verifySnapshots %%f.bpl
-)
+%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl
+
-- 
cgit v1.2.3