Did some refactoring in the execution engine and worked on the parallelization.

5 files changed, 275 insertions, 234 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 7e0e9732..12a6084f 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -37,13 +37,13 @@ namespace Microsoft.Boogie {
         goto END;

       }

       if (CommandLineOptions.Clo.Files.Count == 0) {

-        ExecutionEngine.printer.ErrorWriteLine("*** Error: No input files were specified.");

+        ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified.");

         goto END;

       }

       if (CommandLineOptions.Clo.XmlSink != null) {

         string errMsg = CommandLineOptions.Clo.XmlSink.Open();

         if (errMsg != null) {

-          ExecutionEngine.printer.ErrorWriteLine("*** Error: " + errMsg);

+          ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: " + errMsg);

           goto END;

         }

       }

@@ -84,7 +84,7 @@ namespace Microsoft.Boogie {
           extension = extension.ToLower();

         }

         if (extension != ".bpl") {

-          ExecutionEngine.printer.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,

+          ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,

               extension == null ? "" : extension);

           goto END;

         }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 347642d1..a2eb52c8 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -6,6 +6,7 @@ using System.IO;
 using System.Linq;

 using System.Text.RegularExpressions;

 using System.Threading;

+using System.Threading.Tasks;

 using VC;

 using BoogiePL = Microsoft.Boogie;

 

@@ -17,24 +18,24 @@ namespace Microsoft.Boogie
 

   public interface OutputPrinter

   {

-    void ErrorWriteLine(string s);

-    void ErrorWriteLine(string format, params object[] args);

+    void ErrorWriteLine(TextWriter tw, string s);

+    void ErrorWriteLine(TextWriter tw, string format, params object[] args);

     void AdvisoryWriteLine(string format, params object[] args);

-    void Inform(string s);

+    void Inform(string s, TextWriter tw);

     void WriteTrailer(PipelineStatistics stats);

-    void WriteErrorInformation(ErrorInformation errorInfo);

-    void ReportBplError(IToken tok, string message, bool error, string category = null);

+    void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true);

+    void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null);

   }

 

 

   public class ConsolePrinter : OutputPrinter

   {

-    public void ErrorWriteLine(string s)

+    public void ErrorWriteLine(TextWriter tw, string s)

     {

       Contract.Requires(s != null);

       if (!s.Contains("Error: ") && !s.Contains("Error BP"))

       {

-        Console.WriteLine(s);

+        tw.WriteLine(s);

         return;

       }

 

@@ -53,21 +54,21 @@ namespace Microsoft.Boogie
 

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

-      Console.WriteLine(s);

+      tw.WriteLine(s);

       Console.ForegroundColor = col;

 

       if (remaining != null)

       {

-        Console.WriteLine(remaining);

+        tw.WriteLine(remaining);

       }

     }

 

 

-    public void ErrorWriteLine(string format, params object[] args)

+    public void ErrorWriteLine(TextWriter tw, string format, params object[] args)

     {

       Contract.Requires(format != null);

       string s = string.Format(format, args);

-      ErrorWriteLine(s);

+      ErrorWriteLine(tw, s);

     }

 

 

@@ -85,11 +86,11 @@ namespace Microsoft.Boogie
     /// Inform the user about something and proceed with translation normally.

     /// Print newline after the message.

     /// </summary>

-    public void Inform(string s)

+    public void Inform(string s, TextWriter tw)

     {

       if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)

       {

-        Console.WriteLine(s);

+        tw.WriteLine(s);

       }

     }

 

@@ -125,20 +126,26 @@ namespace Microsoft.Boogie
     }

 

 

-    public void WriteErrorInformation(ErrorInformation errorInfo)

+    public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true)

     {

       Contract.Requires(errorInfo != null);

 

-      ReportBplError(errorInfo.Tok, errorInfo.FullMsg, true);

+      ReportBplError(errorInfo.Tok, errorInfo.FullMsg, true, tw);

 

       foreach (var e in errorInfo.Aux)

       {

-        ReportBplError(e.Tok, e.FullMsg, false);

+        if (!(skipExecutionTrace && e.Category.Contains("Execution trace")))

+        {

+          ReportBplError(e.Tok, e.FullMsg, false, tw);

+        }

       }

+

+      tw.Write(errorInfo.Out.ToString());

+      tw.Flush();

     }

 

 

-    public virtual void ReportBplError(IToken tok, string message, bool error, string category = null)

+    public virtual void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null)

     {

       Contract.Requires(message != null);

 

@@ -157,11 +164,11 @@ namespace Microsoft.Boogie
       }

       if (error)

       {

-        ErrorWriteLine(s);

+        ErrorWriteLine(tw, s);

       }

       else

       {

-        Console.WriteLine(s);

+        tw.WriteLine(s);

       }

     }

   }

@@ -227,6 +234,7 @@ namespace Microsoft.Boogie
     public string RequestId { get; set; }

     public ErrorKind Kind { get; set; }

     public string ImplementationName { get; set; }

+    public TextWriter Out = new StringWriter();

 

     public string FullMsg

     {

@@ -497,7 +505,7 @@ namespace Microsoft.Boogie
     public static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)

     {

       Contract.Requires(cce.NonNullElements(fileNames));

-      //BoogiePL.Errors.count = 0;

+

       Program program = null;

       bool okay = true;

       for (int fileId = 0; fileId < fileNames.Count; fileId++)

@@ -530,7 +538,7 @@ namespace Microsoft.Boogie
         }

         catch (IOException e)

         {

-          printer.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);

+          printer.ErrorWriteLine(Console.Out, "Error opening file \"{0}\": {1}", bplFileName, e.Message);

           okay = false;

           continue;

         }

@@ -655,31 +663,22 @@ namespace Microsoft.Boogie
         }

         if (inline)

         {

-          foreach (var d in TopLevelDeclarations)

+          foreach (var impl in TopLevelDeclarations.OfType<Implementation>())

           {

-            var impl = d as Implementation;

-            if (impl != null)

-            {

-              impl.OriginalBlocks = impl.Blocks;

-              impl.OriginalLocVars = impl.LocVars;

-            }

+            impl.OriginalBlocks = impl.Blocks;

+            impl.OriginalLocVars = impl.LocVars;

           }

-          foreach (var d in TopLevelDeclarations)

+          foreach (var impl in TopLevelDeclarations.OfType<Implementation>())

           {

-            var impl = d as Implementation;

-            if (impl != null && !impl.SkipVerification)

+            if (!impl.SkipVerification)

             {

               Inliner.ProcessImplementation(program, impl);

             }

           }

-          foreach (var d in TopLevelDeclarations)

+          foreach (var impl in TopLevelDeclarations.OfType<Implementation>())

           {

-            var impl = d as Implementation;

-            if (impl != null)

-            {

-              impl.OriginalBlocks = null;

-              impl.OriginalLocVars = null;

-            }

+            impl.OriginalBlocks = null;

+            impl.OriginalLocVars = null;

           }

         }

       }

@@ -755,36 +754,6 @@ namespace Microsoft.Boogie
       }

       #endregion

 

-      #region Set up the VC generation

-

-      ConditionGeneration vcgen = null;

-      try

-      {

-        if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

-        {

-          vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

-        else if (CommandLineOptions.Clo.FixedPointEngine != null)

-        {

-          vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

-        else if (CommandLineOptions.Clo.StratifiedInlining > 0)

-        {

-          vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

-        else

-        {

-          vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

-      }

-      catch (ProverException e)

-      {

-        printer.ErrorWriteLine("Fatal Error: ProverException: {0}", e);

-        return PipelineOutcome.FatalError;

-      }

-

-      #endregion

-

       #region Select and prioritize implementations that should be verified

 

       var impls = program.TopLevelDeclarations.OfType<Implementation>().Where(

@@ -807,141 +776,198 @@ namespace Microsoft.Boogie
 

       #region Verify each implementation

 

-      foreach (var impl in stablePrioritizedImpls)

-      {

-        VerificationResult verificationResult = null;

-

-        printer.Inform(string.Format("\nVerifying {0} ...", impl.Name));

-

-        if (CommandLineOptions.Clo.VerifySnapshots)

-        {

-          verificationResult = Cache.Lookup(impl);

-        }

+      var outputs = new StringWriter[stablePrioritizedImpls.Count()];

+      var nextPrintableIndex = 0;

 

-        if (verificationResult != null)

-        {

-          if (CommandLineOptions.Clo.XmlSink != null)

-          {

-            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);

-          }

-

-          printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name));

-        }

-        else

+      try

+      {

+        Parallel.For(0, stablePrioritizedImpls.Count(), new ParallelOptions { MaxDegreeOfParallelism = 1 }, index =>

         {

-          #region Verify the implementation

+          Implementation impl = stablePrioritizedImpls[index];

+          VerificationResult verificationResult = null;

+          var output = new StringWriter();

 

-          verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);

-          verificationResult.ImplementationName = impl.Name;

-          verificationResult.ImplementationToken = impl.tok;

-          verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;

-          verificationResult.Start = DateTime.UtcNow;

+          printer.Inform(string.Format("\nVerifying {0} ...", impl.Name), output);

 

-          if (CommandLineOptions.Clo.XmlSink != null)

+          if (CommandLineOptions.Clo.VerifySnapshots)

           {

-            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);

+            verificationResult = Cache.Lookup(impl);

           }

 

-          try

+          if (verificationResult != null)

           {

-            if (CommandLineOptions.Clo.inferLeastForUnsat != null)

+            if (CommandLineOptions.Clo.XmlSink != null)

             {

-              var svcgen = vcgen as VC.StratifiedVCGen;

-              Contract.Assert(svcgen != null);

-              var ss = new HashSet<string>();

-              foreach (var tdecl in program.TopLevelDeclarations)

-              {

-                var c = tdecl as Constant;

-                if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

-                ss.Add(c.Name);

-              }

-              verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);

-              verificationResult.Errors = new List<Counterexample>();

-              Console.WriteLine("Result: {0}", string.Join(" ", ss));

+              CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);

             }

-            else

+

+            printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);

+          }

+          else

+          {

+            #region Verify the implementation

+

+            verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);

+            verificationResult.ImplementationName = impl.Name;

+            verificationResult.ImplementationToken = impl.tok;

+

+            using (var vcgen = CreateVCGen(program))

             {

-              verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId);

+              verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;

+              verificationResult.Start = DateTime.UtcNow;

 

-              if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null)

+              if (CommandLineOptions.Clo.XmlSink != null)

               {

-                var vcg = vcgen as VCGen;

-                if (vcg != null)

+                CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);

+              }

+              try

+              {

+                if (CommandLineOptions.Clo.inferLeastForUnsat != null)

                 {

-                  for (int i = 0; i < verificationResult.Errors.Count; i++)

+                  var svcgen = vcgen as VC.StratifiedVCGen;

+                  Contract.Assert(svcgen != null);

+                  var ss = new HashSet<string>();

+                  foreach (var tdecl in program.TopLevelDeclarations)

                   {

-                    verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name, program, extractLoopMappingInfo);

+                    var c = tdecl as Constant;

+                    if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

+                    ss.Add(c.Name);

+                  }

+                  verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);

+                  verificationResult.Errors = new List<Counterexample>();

+                  output.WriteLine("Result: {0}", string.Join(" ", ss));

+                }

+                else

+                {

+                  verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId);

+                  if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null)

+                  {

+                    var vcg = vcgen as VCGen;

+                    if (vcg != null)

+                    {

+                      for (int i = 0; i < verificationResult.Errors.Count; i++)

+                      {

+                        verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name, program, extractLoopMappingInfo);

+                      }

+                    }

                   }

                 }

               }

-            }

-          }

-          catch (VCGenException e)

-          {

-            var errorInfo = errorInformationFactory.CreateErrorInformation(impl.tok, String.Format("{0} (encountered in implementation {1}).", e.Message, impl.Name), requestId, "Error");

-            errorInfo.BoogieErrorCode = "BP5010";

-            errorInfo.ImplementationName = impl.Name;

-            printer.WriteErrorInformation(errorInfo);

-            if (er != null)

-            {

-              lock (er)

+              catch (VCGenException e)

+              {

+                var errorInfo = errorInformationFactory.CreateErrorInformation(impl.tok, String.Format("{0} (encountered in implementation {1}).", e.Message, impl.Name), requestId, "Error");

+                errorInfo.BoogieErrorCode = "BP5010";

+                errorInfo.ImplementationName = impl.Name;

+                printer.WriteErrorInformation(errorInfo, output);

+                if (er != null)

+                {

+                  lock (er)

+                  {

+                    er(errorInfo);

+                  }

+                }

+                verificationResult.Errors = null;

+                verificationResult.Outcome = VCGen.Outcome.Inconclusive;

+              }

+              catch (UnexpectedProverOutputException upo)

               {

-                er(errorInfo);

+                printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

+                verificationResult.Errors = null;

+                verificationResult.Outcome = VCGen.Outcome.Inconclusive;

               }

+

+              verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;

+              verificationResult.End = DateTime.UtcNow;

             }

-            verificationResult.Errors = null;

-            verificationResult.Outcome = VCGen.Outcome.Inconclusive;

-          }

-          catch (UnexpectedProverOutputException upo)

-          {

-            printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

-            verificationResult.Errors = null;

-            verificationResult.Outcome = VCGen.Outcome.Inconclusive;

+

+            #endregion

+

+            #region Cache the verification result

+

+            if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))

+            {

+              Cache.Insert(impl.Id, verificationResult);

+            }

+

+            #endregion

           }

 

-          verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;

-          verificationResult.End = DateTime.UtcNow;

+          #region Process the verification results and statistics

 

-          #endregion

+          ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);

 

-          #region Cache the verification result

+          ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);

 

-          if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))

+          if (CommandLineOptions.Clo.XmlSink != null)

           {

-            Cache.Insert(impl.Id, verificationResult);

+            CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start);

           }

 

-          #endregion

-        }

+          outputs[index] = output;

 

-        #region Process the verification results and statistics

+          lock (outputs)

+          {

+            for (; nextPrintableIndex < stablePrioritizedImpls.Count() && outputs[nextPrintableIndex] != null; nextPrintableIndex++)

+            {

+              Console.Write(outputs[nextPrintableIndex].ToString());

+              Console.Out.Flush();

+            }

+          }

 

-        ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);

+          if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)

+          {

+            Console.Out.Flush();

+          }

 

-        ProcessErrors(verificationResult.Errors, verificationResult.Outcome, er, impl);

+          #endregion

+        });

+      }

+      catch (ProverException e)

+      {

+        printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);

+        return PipelineOutcome.FatalError;

+      }

 

-        if (CommandLineOptions.Clo.XmlSink != null)

-        {

-          CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start);

-        }

+      cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

 

-        if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)

+      lock (outputs)

+      {

+        for (; nextPrintableIndex < stablePrioritizedImpls.Count() && nextPrintableIndex != null; nextPrintableIndex++)

         {

+          Console.Write(outputs[nextPrintableIndex].ToString());

           Console.Out.Flush();

         }

-

-        #endregion

       }

 

-      vcgen.Close();

-      cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

-

       #endregion

 

       return PipelineOutcome.VerificationCompleted;

     }

 

 

+    private static ConditionGeneration CreateVCGen(Program program)

+    {

+      ConditionGeneration vcgen = null;

+      if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

+      {

+        vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+      }

+      else if (CommandLineOptions.Clo.FixedPointEngine != null)

+      {

+        vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+      }

+      else if (CommandLineOptions.Clo.StratifiedInlining > 0)

+      {

+        vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+      }

+      else

+      {

+        vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+      }

+      return vcgen;

+    }

+

+

     #region Houdini

 

     private static PipelineOutcome RunHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)

@@ -984,8 +1010,8 @@ namespace Microsoft.Boogie
 

       foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)

       {

-        ProcessOutcome(x.outcome, x.errors, "", stats, er);

-        ProcessErrors(x.errors, x.outcome, er);

+        ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, er);

+        ProcessErrors(x.errors, x.outcome, Console.Out, er);

       }

       //errorCount = outcome.ErrorCount;

       //verified = outcome.Verified;

@@ -1011,8 +1037,8 @@ namespace Microsoft.Boogie
       // Run Abstract Houdini

       var abs = new Houdini.AbsHoudini(program, domain);

       var absout = abs.ComputeSummaries();

-      ProcessOutcome(absout.outcome, absout.errors, "", stats, er);

-      ProcessErrors(absout.errors, absout.outcome, er);

+      ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, er);

+      ProcessErrors(absout.errors, absout.outcome, Console.Out, er);

 

       //Houdini.PredicateAbs.Initialize(program);

       //var abs = new Houdini.AbstractHoudini(program);

@@ -1040,26 +1066,26 @@ namespace Microsoft.Boogie
 

 

     private static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,

-                                       PipelineStatistics stats, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)

+                                       PipelineStatistics stats, TextWriter tw, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)

     {

       Contract.Requires(stats != null);

 

       UpdateStatistics(stats, outcome, errors);

 

-      printer.Inform(timeIndication + OutcomeIndication(outcome, errors));

+      printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);

 

-      ReportOutcome(outcome, er, implName, implTok, requestId);

+      ReportOutcome(outcome, er, implName, implTok, requestId, tw);

     }

 

 

-    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId)

+    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw)

     {

       ErrorInformation errorInfo = null;

 

       switch (outcome)

       {

         case VCGen.Outcome.ReachedBound:

-          Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));

+          tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));

           break;

         case VCGen.Outcome.TimedOut:

           if (implName != null && implTok != null)

@@ -1081,12 +1107,15 @@ namespace Microsoft.Boogie
           break;

       }

 

-      if (er != null && errorInfo != null)

+      if (errorInfo != null)

       {

         errorInfo.ImplementationName = implName;

-        lock (er)

+        if (er != null)

         {

-          er(errorInfo);

+          lock (er)

+          {

+            er(errorInfo);

+          }

         }

       }

     }

@@ -1162,7 +1191,7 @@ namespace Microsoft.Boogie
     }

 

 

-    private static void ProcessErrors(List<Counterexample> errors, VC.VCGen.Outcome outcome, ErrorReporterDelegate er, Implementation impl = null)

+    private static void ProcessErrors(List<Counterexample> errors, VC.VCGen.Outcome outcome, TextWriter tw, ErrorReporterDelegate er, Implementation impl = null)

     {

       var implName = impl != null ? impl.Name : null;

 

@@ -1174,8 +1203,6 @@ namespace Microsoft.Boogie
           var errorInfo = CreateErrorInformation(error, outcome);

           errorInfo.ImplementationName = implName;

 

-          printer.WriteErrorInformation(errorInfo);

-

           if (CommandLineOptions.Clo.XmlSink != null)

           {

             WriteErrorInformationToXmlSink(errorInfo, error.Trace);

@@ -1186,18 +1213,21 @@ namespace Microsoft.Boogie
             foreach (string info in error.relatedInformation)

             {

               Contract.Assert(info != null);

-              Console.WriteLine("       " + info);

+              errorInfo.Out.WriteLine("       " + info);

             }

           }

           if (CommandLineOptions.Clo.ErrorTrace > 0)

           {

-            Console.WriteLine("Execution trace:");

-            error.Print(4, b => { errorInfo.AddAuxInfo(b.tok, b.Label, "Execution trace"); });

+            errorInfo.Out.WriteLine("Execution trace:");

+            error.Print(4, errorInfo.Out, b => { errorInfo.AddAuxInfo(b.tok, b.Label, "Execution trace"); });

           }

           if (CommandLineOptions.Clo.ModelViewFile != null)

           {

-            error.PrintModel();

+            error.PrintModel(errorInfo.Out);

           }

+

+          printer.WriteErrorInformation(errorInfo, tw);

+

           if (er != null)

           {

             lock (er)

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 6897a982..a0454229 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -4,6 +4,7 @@
 //

 //-----------------------------------------------------------------------------

 using System;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Threading;

@@ -159,54 +160,38 @@ namespace Microsoft.Boogie {
 

     private static void Setup(Program prog, ProverContext ctx)

     {

-        // set up the context

-        foreach (Declaration decl in prog.TopLevelDeclarations)

+      // set up the context

+      foreach (Declaration decl in prog.TopLevelDeclarations.ToList())

+      {

+        Contract.Assert(decl != null);

+        var typeDecl = decl as TypeCtorDecl;

+        var constDecl = decl as Constant;

+        var funDecl = decl as Function;

+        var axiomDecl = decl as Axiom;

+        var glVarDecl = decl as GlobalVariable;

+        if (typeDecl != null)

         {

-            Contract.Assert(decl != null);

-            TypeCtorDecl t = decl as TypeCtorDecl;

-            if (t != null)

-            {

-                ctx.DeclareType(t, null);

-            }

+          ctx.DeclareType(typeDecl, null);

         }

-        foreach (Declaration decl in prog.TopLevelDeclarations)

+        else if (constDecl != null)

         {

-            Contract.Assert(decl != null);

-            Constant c = decl as Constant;

-            if (c != null)

-            {

-                ctx.DeclareConstant(c, c.Unique, null);

-            }

-            else

-            {

-                Function f = decl as Function;

-                if (f != null)

-                {

-                    ctx.DeclareFunction(f, null);

-                }

-            }

+          ctx.DeclareConstant(constDecl, constDecl.Unique, null);

         }

-        foreach (Declaration decl in prog.TopLevelDeclarations)

+        else if (funDecl != null)

         {

-            Contract.Assert(decl != null);

-            Axiom ax = decl as Axiom;

-            if (ax != null)

-            {

-                ctx.AddAxiom(ax, null);

-            }

+          ctx.DeclareFunction(funDecl, null);

         }

-        foreach (Declaration decl in prog.TopLevelDeclarations)

+        else if (axiomDecl != null)

         {

-            Contract.Assert(decl != null);

-            GlobalVariable v = decl as GlobalVariable;

-            if (v != null)

-            {

-                ctx.DeclareGlobalVariable(v, null);

-            }

+          ctx.AddAxiom(axiomDecl, null);

         }

+        else if (glVarDecl != null)

+        {

+          ctx.DeclareGlobalVariable(glVarDecl, null);

+        }

+      }

     }

 

-

     /// <summary>

     /// Clean-up.

     /// </summary>

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 3ae97bdd..bcafb9cb 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -4,6 +4,7 @@
 //

 //-----------------------------------------------------------------------------

 using System;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics;

@@ -147,14 +148,14 @@ namespace Microsoft.Boogie {
         return naryExpr.Fun.FunctionName;

     }

 

-    public void Print(int indent, Action<Block> blockAction = null) {

+    public void Print(int indent, TextWriter tw, Action<Block> blockAction = null) {

       int numBlock = -1;

       string ind = new string(' ', indent);

       foreach (Block b in Trace) {

         Contract.Assert(b != null);

         numBlock++;

         if (b.tok == null) {

-          Console.WriteLine("{0}<intermediate block>", ind);

+          tw.WriteLine("{0}<intermediate block>", ind);

         } else {

           // for ErrorTrace == 1 restrict the output;

           // do not print tokens with -17:-4 as their location because they have been

@@ -165,7 +166,7 @@ namespace Microsoft.Boogie {
                 blockAction(b);

             }

 

-            Console.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);

+            tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);

 

             for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)

             {

@@ -178,13 +179,13 @@ namespace Microsoft.Boogie {
                     {

                         Contract.Assert(calleeCounterexamples[loc].args.Count == 1);

                         var arg = calleeCounterexamples[loc].args[0];

-                        Console.WriteLine("{0}value = {1}", ind, arg.ToString());

+                        tw.WriteLine("{0}value = {1}", ind, arg.ToString());

                     }

                     else

                     {

-                        Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);

-                        calleeCounterexamples[loc].counterexample.Print(indent + 4);

-                        Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);

+                        tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);

+                        calleeCounterexamples[loc].counterexample.Print(indent + 4, tw);

+                        tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);

                     }

                 }

             }

@@ -197,7 +198,7 @@ namespace Microsoft.Boogie {
 

     public bool ModelHasStatesAlready = false;

 

-    public void PrintModel()

+    public void PrintModel(TextWriter tw)

     {

       var filename = CommandLineOptions.Clo.ModelViewFile;

       if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;

@@ -205,8 +206,8 @@ namespace Microsoft.Boogie {
       var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();

 

       if (filename == "-") {

-        m.Write(Console.Out);

-        Console.Out.Flush();

+        m.Write(tw);

+        tw.Flush();

       } else {

         using (var wr = new StreamWriter(filename, !firstModelFile)) {

           firstModelFile = false;

@@ -532,7 +533,7 @@ namespace VC {
   }

 

   [ContractClass(typeof(ConditionGenerationContracts))]

-  public abstract class ConditionGeneration {

+  public abstract class ConditionGeneration : IDisposable {

     protected internal object CheckerCommonState;

 

     public enum Outcome {

@@ -570,6 +571,9 @@ namespace VC {
     public int CumulativeAssertionCount;  // for statistics

 

     protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();

+

+    private bool _disposed;

+

     protected VariableSeq CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

@@ -1626,6 +1630,24 @@ namespace VC {
       #endregion

     }

 

+

+    public void Dispose()

+    {

+      Dispose(true);

+      GC.SuppressFinalize(this);

+    }

+

+    protected virtual void Dispose(bool disposing)

+    {

+      if (!_disposed)

+      {

+        if (disposing)

+        {

+          Close();

+        }

+        _disposed = true;

+      }

+    }

   }

 

   public class ModelViewInfo

@@ -1643,10 +1665,10 @@ namespace VC {
       Contract.Requires(impl != null);

 

       // global variables

-      foreach (Declaration d in program.TopLevelDeclarations) {

-        if (d is Constant) continue;

-        if (d is Variable) {

-          AllVariables.Add((Variable)d);

+      foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>()) {

+        if (!(v is Constant))

+        {

+          AllVariables.Add(v);

         }

       }

       // implementation parameters

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 6a0891b8..bea79f13 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1410,7 +1410,11 @@ namespace VC {
       }

 

       ModelViewInfo mvInfo;

-      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

+      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;

+      lock (program)

+      {

+        gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

+      }

 

       double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;

       int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits,