summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/VC.cs')
-rw-r--r--Source/VCGeneration/VC.cs8
1 files changed, 0 insertions, 8 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index d40b1008..4a89156b 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -317,10 +317,6 @@ namespace VC {
ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
ch.ProverTask.Wait();
}
- catch
- {
- throw;
- }
finally
{
ch.GoBackToIdle();
@@ -1568,10 +1564,6 @@ namespace VC {
break;
}
}
- catch
- {
- throw;
- }
finally
{
s.Checker.GoBackToIdle();