summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/ConditionGeneration.cs
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-07-10 13:47:44 +0200
committerGravatar wuestholz <unknown>2014-07-10 13:47:44 +0200
commit9abbf5e9060e152fb13c0cd5c9fbbdc3aba19f30 (patch)
treedd4ee649076e5b1a0db2cdc40542554a7f54be22 /Source/VCGeneration/ConditionGeneration.cs
parent5e52d81030d85b76cc6a0209617af8c21159755d (diff)
Worked on the more advanced verification result caching.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs6
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);
}