From 82bf08e30124735b41ea901530ce40ef4944c9c9 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Fri, 5 Jun 2015 12:09:49 +0200
Subject: Improve support for diagnosing timeouts.

---
 Source/VCGeneration/Check.cs               |  3 ++-
 Source/VCGeneration/ConditionGeneration.cs | 11 ++++++++---
 2 files changed, 10 insertions(+), 4 deletions(-)

(limited to 'Source/VCGeneration')

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;
           }
-- 
cgit v1.2.3