summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VCDoomed.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/VCDoomed.cs')
-rw-r--r--Source/VCGeneration/VCDoomed.cs4
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index 734d81d6..4d2e0775 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -121,7 +121,9 @@ namespace VC {
Checker checker = FindCheckerFor(impl, 1000);
Contract.Assert(checker != null);
- DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks);
+ int assertionCount;
+ DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);
+ CumulativeAssertionCount += assertionCount;
//EmitImpl(impl, false);