summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
diff options
context:
space:
mode:
Diffstat (limited to 'Test/VSI-Benchmarks/runtestRuntimeChecking.bat')
-rw-r--r--Test/VSI-Benchmarks/runtestRuntimeChecking.bat2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
index 8ac0f707..27df70a3 100644
--- a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
+++ b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
@@ -14,7 +14,7 @@ REM b6: functions
for %%f in (b1 b3 b7 b8) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /nologo /errorTrace:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
+ %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy
if exist %%f.cs. (
del %%f.cs
)