diff options
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index f5469ebf..c3134c09 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -149,6 +149,12 @@ namespace VC { 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);
+ }
+
// Label the assume if it is a procedure call
NAryExpr naryExpr = ac.Expr as NAryExpr;
if (naryExpr != null) {
|