4 files changed, 139 insertions, 0 deletions
diff --git a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking
new file mode 100644
index 00000000..debe2cd3
--- /dev/null
+++ b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking
@@ -0,0 +1,49 @@
+
+-------------------- b1 --------------------
+
+Dafny program verifier finished with 10 verified, 0 errors
+Compiled assembly into b1.exe
+
+-------------------- b2 --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
+Compiled assembly into b2.exe
+
+-------------------- b3 --------------------
+b3.dfy(114,28): Error BP5005: This loop invariant might not be maintained by the loop.
+
+Dafny program verifier finished with 9 verified, 1 error
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+
+-------------------- b4 --------------------
+
+Dafny program verifier finished with 11 verified, 0 errors
+Compiled assembly into b4.dll
+
+-------------------- b5 --------------------
+
+Dafny program verifier finished with 22 verified, 0 errors
+Compiled assembly into b5.dll
+
+-------------------- b6 --------------------
+
+Dafny program verifier finished with 21 verified, 0 errors
+Compiled assembly into b6.exe
+
+-------------------- b7 --------------------
+
+Dafny program verifier finished with 23 verified, 0 errors
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Client.Sort has no body
+
+-------------------- b8 --------------------
+
+Dafny program verifier finished with 42 verified, 0 errors
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Glossary.Sort has no body
diff --git a/Test/VSI-Benchmarks/AnswerRuntimeChecking b/Test/VSI-Benchmarks/AnswerRuntimeChecking
new file mode 100644
index 00000000..841a04cf
--- /dev/null
+++ b/Test/VSI-Benchmarks/AnswerRuntimeChecking
@@ -0,0 +1,30 @@
+
+-------------------- b1 --------------------
+
+Dafny program verifier finished with 10 verified, 0 errors
+Compiled assembly into b1.exe
+Rewrote assembly into b1.exe
+
+-------------------- b3 --------------------
+b3.dfy(114,28): Error BP5005: This loop invariant might not be maintained by the loop.
+
+Dafny program verifier finished with 9 verified, 1 error
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+
+-------------------- b7 --------------------
+
+Dafny program verifier finished with 23 verified, 0 errors
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Client.Sort has no body
+
+-------------------- b8 --------------------
+
+Dafny program verifier finished with 42 verified, 0 errors
+Compilation error: Method _default.Queue.Init has no body
+Compilation error: Method _default.Queue.Enqueue has no body
+Compilation error: Method _default.Queue.Dequeue has no body
+Compilation error: Method _default.Glossary.Sort has no body
diff --git a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
new file mode 100644
index 00000000..ccf1ffa8
--- /dev/null
+++ b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
@@ -0,0 +1,27 @@
+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+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
+  if exist %%f.cs. (
+    del %%f.cs
+  )
+  if exist %%f.exe. (
+    del %%f.exe
+  )
+  if exist %%f.dll. (
+    del %%f.dll
+  )
+  if exist %%f.pdb. (
+    del %%f.pdb
+  )
+  if exist %%f.pdb.original. (
+    del %%f.pdb.original
+  )
+)
diff --git a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
new file mode 100644
index 00000000..8ac0f707
--- /dev/null
+++ b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
@@ -0,0 +1,33 @@
+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+REM to implement:
+REM b2: quantifiers
+REM b4: old expressions
+REM b5: parallel statements
+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
+  if exist %%f.cs. (
+    del %%f.cs
+  )
+  if exist %%f.exe. (
+    del %%f.exe
+  )
+  if exist %%f.dll. (
+    del %%f.dll
+  )
+  if exist %%f.pdb. (
+    del %%f.pdb
+  )
+  if exist %%f.pdb.original. (
+    del %%f.pdb.original
+  )
+)