changed inlining code so that candidate preconditions and postconditions are ignored

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index a202bcfe..adc7e2f0 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -421,7 +421,7 @@ namespace Microsoft.Boogie {
       // inject non-free requires

       for (int i = 0; i < proc.Requires.Length; i++) {

         Requires/*!*/ req = cce.NonNull(proc.Requires[i]);

-        if (!req.Free) {

+        if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {

           Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());

           reqCopy.Condition = codeCopier.CopyExpr(req.Condition);

           AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);

@@ -486,7 +486,7 @@ namespace Microsoft.Boogie {
       // inject non-free ensures

       for (int i = 0; i < proc.Ensures.Length; i++) {

         Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);

-        if (!ens.Free) {

+        if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {

           Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());

           ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);

           AssertCmd/*!*/ a = new AssertEnsuresCmd(ensCopy);