summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/Wlp.cs
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2014-09-29 14:48:54 +0530
committerGravatar akashlal <unknown>2014-09-29 14:48:54 +0530
commitda562b87ac4c5757ed7babbab1aef5b510963c68 (patch)
tree20b386cb93a9b0b8c3cabde1571b4bf472227b72 /Source/VCGeneration/Wlp.cs
parentc70a5e1956554c40f35f0f5a5d5f02f456c00ce9 (diff)
Cleanup: removed unused code
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
-rw-r--r--Source/VCGeneration/Wlp.cs7
1 files changed, 1 insertions, 6 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index c9b7ae83..c6cebdab 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -147,12 +147,7 @@ namespace VC {
} else if (cmd is AssumeCmd) {
AssumeCmd ac = (AssumeCmd)cmd;
- if (CommandLineOptions.Clo.StratifiedInlining > 0) {
- var pname = QKeyValue.FindStringAttribute(ac.Attributes, "candidate");
- if (pname != null) {
- return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
- }
-
+ if (CommandLineOptions.Clo.StratifiedInlining > 0) {
// Label the assume if it is a procedure call
NAryExpr naryExpr = ac.Expr as NAryExpr;
if (naryExpr != null) {