From 17f64e094fc0505e2049d0064883f4cffa2cc11b Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Thu, 11 Jul 2013 16:06:26 -0700
Subject: Worked on the parallelization.

---
 Source/Doomed/DoomCheck.cs | 23 ++++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

(limited to 'Source/Doomed')

diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index 7e2ec984..b317dc71 100644
--- a/Source/Doomed/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -115,21 +115,26 @@ void ObjectInvariant()
 
             // Todo: Check if vc is trivial true or false            
             outcome = ProverInterface.Outcome.Undetermined;
-            Contract.Assert( m_ErrorHandler !=null);
-            m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
-            m_Checker.ProverTask.Wait();
-            
-            try {
+            Contract.Assert(m_ErrorHandler != null);
+            try
+            {
+              m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
+              m_Checker.ProverTask.Wait();
               outcome = m_Checker.ReadOutcome();
-              m_Checker.GoBackToIdle();
-            } catch (UnexpectedProverOutputException e)
+            }
+            catch (UnexpectedProverOutputException e)
             {
-              if (CommandLineOptions.Clo.TraceVerify) { 
+              if (CommandLineOptions.Clo.TraceVerify)
+              {
                 Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name);
                 Console.WriteLine(e.ToString());
               }
               return false;
-            }                        
+            }
+            finally
+            {
+              m_Checker.GoBackToIdle();
+            }
             return true;
         }
     }
-- 
cgit v1.2.3