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);