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

2 files changed, 5 insertions, 4 deletions

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);

         }