diff options
Diffstat (limited to 'Test/snapshots/runtest.bat')
| -rw-r--r-- | Test/snapshots/runtest.bat | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat index fa45d56a..663cef07 100644 --- a/Test/snapshots/runtest.bat +++ b/Test/snapshots/runtest.bat @@ -1,17 +1,11 @@ -
@echo off
setlocal
set BOOGIEDIR=..\..\Binaries
set BGEXE=%BOOGIEDIR%\Boogie.exe
-echo -------------------- Snapshots0.bpl --------------------
-%BGEXE% %* /verifySnapshots Snapshots0.bpl
-
-echo.
-echo -------------------- Snapshots1.bpl --------------------
-%BGEXE% %* /verifySnapshots Snapshots1.bpl
-
-echo.
-echo -------------------- Snapshots2.bpl --------------------
-%BGEXE% %* /verifySnapshots Snapshots2.bpl
+for %%f in (Snapshots0 Snapshots1 Snapshots2 Snapshots3) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /verifySnapshots %%f.bpl
+)
|