diff options
Diffstat (limited to 'Source/Doomed/DoomCheck.cs')
| -rw-r--r-- | Source/Doomed/DoomCheck.cs | 23 |
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;
}
}
|