summaryrefslogtreecommitdiff
path: root/Source/Doomed/DoomCheck.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Doomed/DoomCheck.cs')
-rw-r--r--Source/Doomed/DoomCheck.cs23
1 files changed, 14 insertions, 9 deletions
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;
}
}