From 8926e773af99a75fe1b061a55987fa9f42898f75 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Sat, 12 Feb 2011 11:30:12 +0000
Subject: Better support for timeout

---
 Source/VCGeneration/StratifiedVC.cs | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 7cb4b3b4..fda8770c 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -833,6 +833,9 @@ namespace VC
         {
             Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
 
+            // Record current time
+            var startTime = DateTime.Now;
+
             // Get the checker
             Checker checker = FindCheckerFor(impl, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
 
@@ -1001,6 +1004,9 @@ namespace VC
             // Get the checker
             Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
             
+            // Record current time
+            var startTime = DateTime.Now;
+
             // Run live variable analysis
             if (CommandLineOptions.Clo.LiveVariableAnalysis == 2)
             {
@@ -1107,6 +1113,16 @@ namespace VC
             //   case 3: (internal error)   The theorem prover TimesOut of runs OutOfMemory
             while (true)
             {
+                // Check timeout
+                if (CommandLineOptions.Clo.ProverKillTime != -1)
+                {
+                    if ((DateTime.Now - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)
+                    {
+                        ret = Outcome.TimedOut;
+                        break;
+                    }
+                }
+
                 // Note: in the absence of a coverage graph process, the task is always "step"
                 coverageManager.syncGraph();
                 var task = coverageManager.getNextTask();
-- 
cgit v1.2.3