diff options
| author |  qadeer <unknown> | 2014-09-18 09:33:33 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-09-18 09:33:33 -0700 |
| commit | d1d367b1e9fb1cde673332030ef68b230c22dd06 (patch) | |
| tree | ad14b94d32a7fac1c18b872f79294abda3a05384 /Source/Core/Inline.cs | |
| parent | 0c35477ac7e7fb5b73b3c64e301e09cd876c0703 (diff) | |
InlineAssume attribute for ensures clauses; if present, the ensures condition is assumed while inlining.
Diffstat (limited to 'Source/Core/Inline.cs')
| -rw-r--r-- | Source/Core/Inline.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 00aa5631..fe61a765 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -516,7 +516,7 @@ namespace Microsoft.Boogie { }
private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) {
- if (QKeyValue.FindBoolAttribute(ens.Attributes, "HoudiniAssume")) {
+ if (QKeyValue.FindBoolAttribute(ens.Attributes, "InlineAssume")) {
return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
} else if (ens.Free) {
return new AssumeCmd(ens.tok, Expr.True);
|