summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/Wlp.cs
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2013-10-21 19:47:24 +0530
committerGravatar akashlal <unknown>2013-10-21 19:47:24 +0530
commit350ccedd0c5e4816d03ab2c2231ba8012557da74 (patch)
tree3ec09959822e601de9bd31ad338a87250ccae0c4 /Source/VCGeneration/Wlp.cs
parent17bf21691f93d99f63d56a85a5fa3b788a93828c (diff)
Bug fix in stratified inlining (triggered by {:inline} functions)
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
-rw-r--r--Source/VCGeneration/Wlp.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index bb2a2785..c9b7ae83 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -152,7 +152,7 @@ namespace VC {
if (pname != null) {
return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
}
-
+
// Label the assume if it is a procedure call
NAryExpr naryExpr = ac.Expr as NAryExpr;
if (naryExpr != null) {