diff options
| author |  wuestholz <unknown> | 2014-07-10 13:47:44 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-07-10 13:47:44 +0200 |
| commit | 9abbf5e9060e152fb13c0cd5c9fbbdc3aba19f30 (patch) | |
| tree | dd4ee649076e5b1a0db2cdc40542554a7f54be22 /Source/VCGeneration/ConditionGeneration.cs | |
| parent | 5e52d81030d85b76cc6a0209617af8c21159755d (diff) | |
Worked on the more advanced verification result caching.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 25ddc2c0..5304a789 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1538,8 +1538,7 @@ namespace VC { && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
{
// Turn it into an assume statement.
- // TODO(wuestholz): Uncomment this.
- // pc = new AssumeCmd(ac.tok, copy);
+ pc = new AssumeCmd(ac.tok, copy);
pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
}
else if (currentImplementation != null
@@ -1550,8 +1549,7 @@ namespace VC { && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
{
// Turn it into an assume statement.
- // TODO(wuestholz): Uncomment this.
- // pc = new AssumeCmd(ac.tok, copy);
+ pc = new AssumeCmd(ac.tok, copy);
pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);
currentImplementation.AddRecycledFailingAssertion(ac);
}
|