summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
diff options
context:
space:
mode:
Diffstat (limited to 'Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat')
-rw-r--r--Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
index ccf1ffa8..c85b7606 100644
--- a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
+++ b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
@@ -8,7 +8,7 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe
for %%f in (b1 b2 b3 b4 b5 b6 b7 b8) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /nologo /errorTrace:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy
if exist %%f.cs. (
del %%f.cs
)