7 files changed, 6 insertions, 43 deletions
diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer
index dc523fdf..9a083fa3 100644
--- a/Test/VSComp2010/Answer
+++ b/Test/VSComp2010/Answer
@@ -2,24 +2,19 @@
 -------------------- Problem1-SumMax.dfy --------------------
 
 Dafny program verifier finished with 4 verified, 0 errors
-Compiled program written to out.cs
 
 -------------------- Problem2-Invert.dfy --------------------
 
 Dafny program verifier finished with 7 verified, 0 errors
-Compiled program written to out.cs
 
 -------------------- Problem3-FindZero.dfy --------------------
 
 Dafny program verifier finished with 7 verified, 0 errors
-Compiled program written to out.cs
 
 -------------------- Problem4-Queens.dfy --------------------
 
 Dafny program verifier finished with 9 verified, 0 errors
-Compiled program written to out.cs
 
 -------------------- Problem5-DoubleEndedQueue.dfy --------------------
 
 Dafny program verifier finished with 21 verified, 0 errors
-Compiled program written to out.cs
diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
index e16eda13..9535d677 100644
--- a/Test/VSComp2010/runtest.bat
+++ b/Test/VSComp2010/runtest.bat
@@ -11,7 +11,5 @@ for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy
             Problem5-DoubleEndedQueue.dfy) do (
   echo.
   echo -------------------- %%f --------------------
-  %DAFNY_EXE% %* %%f
-
-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+  %DAFNY_EXE% /compile:0 %* %%f
 )
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index a733a1c0..611f9251 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -9,11 +9,5 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (
   echo.
   echo -------------------- %%f --------------------
-
-  REM The following line will just run the verifier
-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f
-
-  REM Alternatively, the following lines also produce C# code and compile it
-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+  %DAFNY_EXE% /compile:0 %* %%f
 )
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 15bd28a1..524765cf 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -26,11 +26,5 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
             UltraFilter.dfy) do (
   echo.
   echo -------------------- %%f --------------------
-
-  REM The following line will just run the verifier
-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-
-  REM Alternatively, the following lines also produce C# code and compile it
-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
 )
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 50b4ca18..6c723ea5 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -16,11 +16,5 @@ for %%f in (
   ) do (
   echo.
   echo -------------------- %%f --------------------
-
-  REM The following line will just run the verifier
-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-
-  REM Alternatively, the following lines also produce C# code and compile it
-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
 )
diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
index 32c6a984..efe7b3d5 100644
--- a/Test/vacid0/runtest.bat
+++ b/Test/vacid0/runtest.bat
@@ -9,11 +9,5 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (
   echo.
   echo -------------------- %%f --------------------
-
-  REM The following line will just run the verifier
-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f
-
-  REM Alternatively, the following lines also produce C# code and compile it
-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+  %DAFNY_EXE% /compile:0 %* %%f
 )
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 07b5859e..5145cb56 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -14,11 +14,5 @@ for %%f in (
   ) do (
   echo.
   echo -------------------- %%f --------------------
-
-  REM The following line will just run the verifier
-  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-
-  REM Alternatively, the following lines also produce C# code and compile it
-  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
-  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+  %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
 )