Merge

13 files changed, 182 insertions, 99 deletions

diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs
index 799a60de..fd69d911 100644
--- a/Source/Core/VariableDependenceAnalyser.cs
+++ b/Source/Core/VariableDependenceAnalyser.cs
@@ -210,7 +210,7 @@ namespace Microsoft.Boogie {
           Console.Write(v);

         }

       }

-      Console.WriteLine("\n");

+      Console.WriteLine(); Console.WriteLine();

     }

 

     public void Analyse() {

diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index 1b78afc3..7e2ec984 100644
--- a/Source/Doomed/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -121,6 +121,7 @@ void ObjectInvariant()
             

             try {

               outcome = m_Checker.ReadOutcome();

+              m_Checker.GoBackToIdle();

             } catch (UnexpectedProverOutputException e)

             {

               if (CommandLineOptions.Clo.TraceVerify) { 

diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index fadb2ea7..778ae767 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -34,8 +34,8 @@ namespace VC {
     /// <summary>

     /// Constructor.  Initializes the theorem prover.

     /// </summary>

-    public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program) {

+    public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, checkers) {

       Contract.Requires(program != null);

 

       this.appendLogFile = appendLogFile;

@@ -115,7 +115,7 @@ namespace VC {
 

       //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));

     

-      Checker checker = FindCheckerFor(impl, 1000);

+      Checker checker = FindCheckerFor(1000);

       Contract.Assert(checker != null);

       int assertionCount;

       DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);

@@ -173,7 +173,7 @@ namespace VC {
         if (restartTP)

         {

             checker.Close();

-            checker = FindCheckerFor(impl, 1000);

+            checker = FindCheckerFor(1000);

             dc.RespawnChecker(impl, checker);

             dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);

         }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 75cd172a..21d0c014 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -776,32 +776,44 @@ namespace Microsoft.Boogie
 

       var outputCollector = new OutputCollector(stablePrioritizedImpls);

       var outcome = PipelineOutcome.VerificationCompleted;

+      var checkers = new List<Checker>();

       var tasks = new Task[stablePrioritizedImpls.Length];

       for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)

       {

         var taskIndex = i;

         var t = Task.Factory.StartNew(() =>

         {

-          VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector);

-        });

+          VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, checkers);

+        }, TaskCreationOptions.LongRunning);

         tasks[taskIndex] = t;

-        try

+      }

+      try

+      {

+        Task.WaitAll(tasks);

+      }

+      catch (AggregateException ae)

+      {

+        ae.Handle(e =>

         {

-          Task.WaitAll(new Task[] { t });

-        }

-        catch (AggregateException ae)

+          var pe = e as ProverException;

+          if (pe != null)

+          {

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

+            outcome = PipelineOutcome.FatalError;

+            return true;

+          }

+          return false;

+        });

+      }

+      finally

+      {

+        lock (checkers)

         {

-          ae.Handle(e =>

+          foreach (Checker checker in checkers)

           {

-            var pe = e as ProverException;

-            if (pe != null)

-            {

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

-              outcome = PipelineOutcome.FatalError;

-              return true;

-            }

-            return false;

-          });

+            Contract.Assert(checker != null);

+            checker.Close();

+          }

         }

       }

 

@@ -815,13 +827,14 @@ namespace Microsoft.Boogie
     }

 

 

-    private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector)

+    private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, List<Checker> checkers)

     {

       Implementation impl = stablePrioritizedImpls[index];

       VerificationResult verificationResult = null;

       var output = new StringWriter();

 

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

+      printer.Inform("", output);  // newline

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

 

       if (CommandLineOptions.Clo.VerifySnapshots)

       {

@@ -845,7 +858,7 @@ namespace Microsoft.Boogie
         verificationResult.ImplementationName = impl.Name;

         verificationResult.ImplementationToken = impl.tok;

 

-        using (var vcgen = CreateVCGen(program))

+        using (var vcgen = CreateVCGen(program, checkers))

         {

           verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;

           verificationResult.Start = DateTime.UtcNow;

@@ -986,24 +999,24 @@ namespace Microsoft.Boogie
     }

 

 

-    private static ConditionGeneration CreateVCGen(Program program)

+    private static ConditionGeneration CreateVCGen(Program program, List<Checker> checkers)

     {

       ConditionGeneration vcgen = null;

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

       {

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

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

       }

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

       {

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

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

       }

       else if (CommandLineOptions.Clo.StratifiedInlining > 0)

       {

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

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

       }

       else

       {

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

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

       }

       return vcgen;

     }

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index a9fae923..24a3c708 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -98,7 +98,7 @@ namespace Microsoft.Boogie.Houdini {
 

             Inline();

 

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

+            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());

             this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);

 

             this.proverTime = TimeSpan.Zero;

@@ -2053,7 +2053,7 @@ namespace Microsoft.Boogie.Houdini {
             if (CommandLineOptions.Clo.ProverKillTime > 0)

                 CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));

 

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

+            this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());

             this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);

 

             this.reporter = new AbstractHoudiniErrorReporter();

diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
index 03f53294..09cef241 100644
--- a/Source/Houdini/CandidateDependenceAnalyser.cs
+++ b/Source/Houdini/CandidateDependenceAnalyser.cs
@@ -310,7 +310,7 @@ namespace Microsoft.Boogie {
       for (int i = 0; i < Components.Count(); i++) {

         Console.Write(i + ": ");

         DumpSCC(Components[i]);

-        Console.WriteLine("\n");

+        Console.WriteLine(); Console.WriteLine();

       }

 

       Console.WriteLine("Stages DAG");

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 4dd985b4..abc5a7e8 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -349,7 +349,7 @@ namespace Microsoft.Boogie.Houdini {
 

       Inline();

 

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

+      this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());

       this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);

 

       vcgenFailures = new HashSet<Implementation>();

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index bc13927f..96dc02a6 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -1179,7 +1179,7 @@ namespace Microsoft.Boogie.SMTLib
 

     public override void SetTimeOut(int ms)

     {

-        SendThisVC("(set-option " + Z3.SetTimeoutOption() + "  " + ms.ToString() + ")\n");

+        SendThisVC("(set-option :" + Z3.SetTimeoutOption() + " " + ms.ToString() + ")");

     }

 

     public override object Evaluate(VCExpr expr)

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 0a1059fe..3249708e 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -18,6 +18,15 @@ using Microsoft.Basetypes;
 using System.Threading.Tasks;

 

 namespace Microsoft.Boogie {

+

+  enum CheckerStatus

+  {

+    Idle,

+    Ready,

+    Busy,

+    Closed

+  }

+

   /// <summary>

   /// Interface to the theorem prover specialized to Boogie.

   ///

@@ -38,18 +47,32 @@ namespace Microsoft.Boogie {
 

     // state for the async interface

     private volatile ProverInterface.Outcome outcome;

-    private volatile bool busy;

     private volatile bool hasOutput;

     private volatile UnexpectedProverOutputException outputExn;

     private DateTime proverStart;

     private TimeSpan proverRunTime;

     private volatile ProverInterface.ErrorHandler handler;

-    private volatile bool closed;

+    private volatile CheckerStatus status;

+    public readonly Program Program;

+

+    public void GetReady()

+    {

+      Contract.Requires(status == CheckerStatus.Idle);

+

+      status = CheckerStatus.Ready;

+    }

+

+    public void GoBackToIdle()

+    {

+      Contract.Requires(IsBusy);

+

+      status = CheckerStatus.Idle;

+    }

 

     public Task ProverTask { get; set; }

 

-    public bool WillingToHandle(Implementation impl, int timeout) {

-      return !closed && timeout == this.timeout;

+    public bool WillingToHandle(int timeout, Program prog) {

+      return status == CheckerStatus.Idle && timeout == this.timeout && (prog == null || Program == prog);

     }

 

     public VCExpressionGenerator VCExprGen {

@@ -107,6 +130,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(vcgen != null);

       Contract.Requires(prog != null);

       this.timeout = timeout;

+      this.Program = prog;

 

       ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();

 

@@ -152,10 +176,18 @@ namespace Microsoft.Boogie {
       this.gen = prover.VCExprGen;

     }

 

-    public void Retarget(Program prog, ProverContext ctx)

+    public void Retarget(Program prog, ProverContext ctx, int timeout = 0)

     {

         ctx.Clear();

         Setup(prog, ctx);

+        if (0 < timeout)

+        {

+          TheoremProver.SetTimeOut(timeout * 1000);

+        }

+        else

+        {

+          TheoremProver.SetTimeOut(0);

+        }

     }

 

     private static void Setup(Program prog, ProverContext ctx)

@@ -195,9 +227,9 @@ namespace Microsoft.Boogie {
     /// <summary>

     /// Clean-up.

     /// </summary>

-    public void Close() {

-      this.closed = true;

+    public void Close() {      

       thmProver.Close();

+      status = CheckerStatus.Closed;

     }

 

     /// <summary>

@@ -212,13 +244,21 @@ namespace Microsoft.Boogie {
 

     public bool IsBusy {

       get {

-        return busy;

+        return status == CheckerStatus.Busy;

       }

     }

 

-    public bool Closed {

+    public bool IsClosed {

       get {

-        return closed;

+        return status == CheckerStatus.Closed;

+      }

+    }

+

+    public bool IsIdle

+    {

+      get

+      {

+        return status == CheckerStatus.Idle;

       }

     }

 

@@ -259,7 +299,6 @@ namespace Microsoft.Boogie {
           break;

       }

 

-      Contract.Assert(busy);

       hasOutput = true;

       proverRunTime = DateTime.UtcNow - proverStart;

     }

@@ -268,10 +307,9 @@ namespace Microsoft.Boogie {
       Contract.Requires(descriptiveName != null);

       Contract.Requires(vc != null);

       Contract.Requires(handler != null);

+      Contract.Requires(status == CheckerStatus.Ready);

 

-      Contract.Requires(!IsBusy);

-      Contract.Assert(!busy);

-      busy = true;

+      status = CheckerStatus.Busy;

       hasOutput = false;

       outputExn = null;

       this.handler = handler;

@@ -280,16 +318,15 @@ namespace Microsoft.Boogie {
       thmProver.BeginCheck(descriptiveName, vc, handler);

       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy

 

-      ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); });

+      ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); } , TaskCreationOptions.LongRunning);

     }

 

     public ProverInterface.Outcome ReadOutcome() {

-

       Contract.Requires(IsBusy);

       Contract.Requires(HasOutput);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+

       hasOutput = false;

-      busy = false;

 

       if (outputExn != null) {

         throw outputExn;

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index bb2deb29..d8af86e4 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -527,8 +527,8 @@ namespace VC {
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       throw new NotImplementedException();

     }

-    public ConditionGenerationContracts(Program p)

-      : base(p) {

+    public ConditionGenerationContracts(Program p, List<Checker> checkers)

+      : base(p, checkers) {

     }

   }

 

@@ -570,7 +570,7 @@ namespace VC {
 

     public int CumulativeAssertionCount;  // for statistics

 

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

+    protected readonly List<Checker>/*!>!*/ checkers;

 

     private bool _disposed;

 

@@ -586,9 +586,11 @@ namespace VC {
 

     public static List<Model> errorModelList;

 

-    public ConditionGeneration(Program p) {

-      Contract.Requires(p != null);

+    public ConditionGeneration(Program p, List<Checker> checkers) {

+      Contract.Requires(p != null && checkers != null && cce.NonNullElements(checkers));

       program = p;

+      this.checkers = checkers;

+      Cores = 1;

     }

 

     /// <summary>

@@ -970,42 +972,61 @@ namespace VC {
     #endregion

 

 

-    protected Checker FindCheckerFor(Implementation impl, int timeout)

+    protected Checker FindCheckerFor(int timeout)

     {

       Contract.Ensures(Contract.Result<Checker>() != null);

 

-      // Look for existing checker.

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

+      lock (checkers)

       {

-        if (checkers[i].Closed)

+      retry:

+        // Look for existing checker.

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

         {

-          checkers.RemoveAt(i);

-          continue;

+          var c = checkers.ElementAt(i);

+          lock (c)

+          {

+            if (c.WillingToHandle(timeout, program))

+            {

+              c.GetReady();

+              return c;

+            }

+            else if (c.IsIdle || c.IsClosed)

+            {

+              if (c.IsIdle)

+              {

+                c.Retarget(program, c.TheoremProver.Context, timeout);

+                return c;

+              }

+              else

+              {

+                checkers.RemoveAt(i);

+              }

+              continue;

+            }

+          }

         }

-        if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout))

+

+        if (Cores <= checkers.Count)

         {

-          return checkers[i];

+          Monitor.Wait(checkers, 50);

+          goto retry;

         }

-      }

 

-      // Create a new checker.

-      string log = logFilePath;

-      if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)

-      {

-        log = log + "." + checkers.Count;

-      }

-      Checker ch = new Checker(this, program, log, appendLogFile, timeout);

-      Contract.Assert(ch != null);

-      checkers.Add(ch);

-      return ch;

+        // Create a new checker.

+        string log = logFilePath;

+        if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)

+        {

+          log = log + "." + checkers.Count;

+        }

+        Checker ch = new Checker(this, program, log, appendLogFile, timeout);

+        ch.GetReady();

+        checkers.Add(ch);

+        return ch;

+      }      

     }

 

 

     virtual public void Close() {

-      foreach (Checker checker in checkers) {

-        Contract.Assert(checker != null);

-        checker.Close();

-      }

     }

 

 

@@ -1655,6 +1676,8 @@ namespace VC {
         _disposed = true;

       }

     }

+

+    public int Cores { get; set; }

   }

 

   public class ModelViewInfo

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 19feabe9..3299ef76 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -78,8 +78,8 @@ namespace Microsoft.Boogie
 

         private static Checker old_checker = null;

 

-        public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile)

-            : base(_program, logFilePath, appendLogFile) 

+        public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+            : base(_program, logFilePath, appendLogFile, checkers) 

         {

             switch (CommandLineOptions.Clo.FixedPointMode)

             {

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 9e0dd798..b4db817f 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -309,8 +309,8 @@ namespace VC {
     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

     public ProverInterface prover;

 

-    public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program, logFilePath, appendLogFile) {

+    public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, logFilePath, appendLogFile, checkers) {

       implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();

       prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);

       foreach (Declaration decl in program.TopLevelDeclarations) {

@@ -510,8 +510,8 @@ namespace VC {
 

     public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree, 

                            HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,

-                           Program program, string/*?*/ logFilePath, bool appendLogFile) 

-    : this(program, logFilePath, appendLogFile)

+                           Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers) 

+    : this(program, logFilePath, appendLogFile, checkers)

     {

       this.procsToSkip = new HashSet<string>(procsToSkip);

       this.extraRecBound = new Dictionary<string, int>(extraRecBound);

@@ -525,8 +525,8 @@ namespace VC {
       }

     }

 

-    public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program, logFilePath, appendLogFile) {

+    public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, logFilePath, appendLogFile, checkers) {

       PersistCallTree = false;

       useSummary = false;

       procsThatReachedRecBound = new HashSet<string>();

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 121cab46..48b73bce 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -26,8 +26,8 @@ namespace VC {
     /// Constructor.  Initializes the theorem prover.

     /// </summary>

     [NotDelayed]

-    public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program)

+    public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, checkers)

     {

       Contract.Requires(program != null);

       this.appendLogFile = appendLogFile;

@@ -291,7 +291,7 @@ namespace VC {
         ModelViewInfo mvInfo;

         parent.PassifyImpl(impl, out mvInfo);

         Hashtable label2Absy;

-        Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);

+        Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);

         Contract.Assert(ch != null);

 

         var exprGen = ch.TheoremProver.Context.ExprGen;

@@ -315,6 +315,7 @@ namespace VC {
         ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));

         ch.ProverTask.Wait();

         ProverInterface.Outcome outcome = ch.ReadOutcome();

+        ch.GoBackToIdle();

         parent.CurrentLocalVariables = null;

 

         DateTime end = DateTime.UtcNow;

@@ -1192,7 +1193,7 @@ namespace VC {
 

         impl.Blocks = blocks;

 

-        checker = parent.FindCheckerFor(impl, timeout);

+        checker = parent.FindCheckerFor(timeout);

         Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();

 

         ProverInterface tp = checker.TheoremProver;

@@ -1201,7 +1202,7 @@ namespace VC {
         bet.SetCodeExprConverter(

           new CodeExprConverter(

           delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {

-            VCGen vcgen = new VCGen(new Program(), null, false);

+            VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);

             vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();

             vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();

             vcgen.CurrentLocalVariables = codeExpr.LocVars;

@@ -1429,7 +1430,7 @@ namespace VC {
 

       Outcome outcome = Outcome.Correct;

 

-      int cores = CommandLineOptions.Clo.VcsCores;

+      Cores = CommandLineOptions.Clo.VcsCores;

       Stack<Split> work = new Stack<Split>();

       List<Split> currently_running = new List<Split>();

       ResetPredecessors(impl.Blocks);

@@ -1450,7 +1451,7 @@ namespace VC {
         bool prover_failed = false;

         Split s;

 

-        if (work.Any() && currently_running.Count < cores) {

+        if (work.Any() && currently_running.Count < Cores) {

           s = work.Pop();

 

           if (first_round && max_splits > 1) {

@@ -1464,10 +1465,13 @@ namespace VC {
             callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));

 

             Contract.Assert(s.parent == this);

-            s.BeginCheck(callback, mvInfo, no, 

-              (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :

-                keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :

-                             CommandLineOptions.Clo.ProverKillTime);

+            lock (program)

+            {

+              s.BeginCheck(callback, mvInfo, no,

+                (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :

+                  keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :

+                               CommandLineOptions.Clo.ProverKillTime);

+            }

 

             no++;

 

@@ -1507,6 +1511,8 @@ namespace VC {
             break;

           }

 

+          s.Checker.GoBackToIdle();

+

           Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);

         }

 

@@ -1550,7 +1556,10 @@ namespace VC {
       }

 

       if (outcome == Outcome.Correct && smoke_tester != null) {

-        smoke_tester.Test();

+        lock (program)

+        {

+          smoke_tester.Test();

+        }

       }

 

       callback.OnProgress("done", 0, 0, 1.0);