diff options
| author |  wuestholz <unknown> | 2013-07-11 16:06:26 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-11 16:06:26 -0700 |
| commit | 17f64e094fc0505e2049d0064883f4cffa2cc11b (patch) | |
| tree | 7e211880e8893792d213a245dfe6b527999c6e9e /Source/Doomed | |
| parent | 37505e4e1c58753012f5694cc27e337934fb9451 (diff) | |
Worked on the parallelization.
Diffstat (limited to 'Source/Doomed')
| -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;
}
}
|