diff options
| author |  Rustan Leino <unknown> | 2014-02-10 18:14:46 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-10 18:14:46 -0800 |
| commit | 8567d68f7f04f87b2d4270e18713bdcdf4d26031 (patch) | |
| tree | 75e633b53ac24d35c2d8d51641736a6b6e22ac99 /Source/VCGeneration/VC.cs | |
| parent | e2feccce72c3f6b6d7ef0ab6c82675e1ff86a5f1 (diff) | |
Fixed errors in the use of Code Contracts
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b0be1072..49ae68e3 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2306,7 +2306,7 @@ namespace VC { Contract.Requires(taskID == -1);
int inductionK = CommandLineOptions.Clo.KInductionDepth;
- Contract.Requires(inductionK >= 0);
+ Contract.Assume(inductionK >= 0);
bool contRuleApplication = true;
while (contRuleApplication) {
|