Improve support for diagnosing timeouts.

2 files changed, 10 insertions, 4 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 7c690eff..33baf798 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -217,6 +217,7 @@ namespace Microsoft.Boogie {
     private void Setup(Program prog, ProverContext ctx)

     {

       Program = prog;

+      // TODO(wuestholz): Is this lock necessary?

       lock (Program.TopLevelDeclarations)

       {

         foreach (Declaration decl in Program.TopLevelDeclarations)

@@ -362,7 +363,7 @@ 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); } , TaskCreationOptions.LongRunning);

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

     }

 

     public ProverInterface.Outcome ReadOutcome() {

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index a19f983a..8d6606b6 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -983,11 +983,11 @@ namespace VC {
     #endregion

 

 

-    protected Checker FindCheckerFor(int timeout, bool isBlocking = true)

+    protected Checker FindCheckerFor(int timeout, bool isBlocking = true, int waitTimeinMs = 50, int maxRetries = 3)

     {

+      Contract.Requires(0 <= waitTimeinMs && 0 <= maxRetries);

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

 

-      var maxRetries = 3;

       lock (checkers)

       {

       retry:

@@ -1015,6 +1015,8 @@ namespace VC {
                 else

                 {

                   checkers.RemoveAt(i);

+                  i--;

+                  continue;

                 }

               }

             }

@@ -1029,7 +1031,10 @@ namespace VC {
         {

           if (isBlocking || 0 < maxRetries)

           {

-            Monitor.Wait(checkers, 50);

+            if (0 < waitTimeinMs)

+            {

+              Monitor.Wait(checkers, waitTimeinMs);

+            }

             maxRetries--;

             goto retry;

           }