summaryrefslogtreecommitdiff
path: root/Test/inline/runtest.bat
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2009-08-07 17:18:14 +0000
committerGravatar rustanleino <unknown>2009-08-07 17:18:14 +0000
commit46b654cd5c5a0dc3df37d9a593fa5c81c59ab83f (patch)
tree8378d2b9e5140c19154e8ceac7ff29e5495efffd /Test/inline/runtest.bat
parent8c24db1994be20528fd0285844ee6a32b847d2aa (diff)
Fixed problem where nullary function with definition had caused a crash.
Diffstat (limited to 'Test/inline/runtest.bat')
-rw-r--r--Test/inline/runtest.bat5
1 files changed, 5 insertions, 0 deletions
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index 3040d5b0..209845e6 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -3,6 +3,11 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
+for %%f in (test0.bpl) do (
+ echo -------------------- %%f --------------------
+ %BGEXE% %* %%f
+)
+
for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* /inline:b /print:- /env:0 /printInlined /noinfer %%f