summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2010-09-05 15:31:56 +0000
committerGravatar akashlal <unknown>2010-09-05 15:31:56 +0000
commit34b52bfc6d4e62a7e8f8c71839952a386b372de2 (patch)
treea358a91917e943cba937973f4175403ff34f4071 /Source/VCGeneration/ConditionGeneration.cs
parent07f7c5bd1600d1fbe90eba8f8f150fe526626568 (diff)
Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal that it has reached the recursion bound.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs3
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index c7761a37..dc13725f 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -360,7 +360,8 @@ namespace VC {
Errors,
TimedOut,
OutOfMemory,
- Inconclusive
+ Inconclusive,
+ ReachedBound
}
[ContractInvariantMethod]