1 files changed, 8 insertions, 1 deletions
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 2150f72d..834099ff 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -494,11 +494,18 @@ public class SmartBlockPredicator {
               .ToArray());
 
           if (impl == null) {
+            var fpIdentifierExpr = new IdentifierExpr(Token.NoToken, fpVar);
             foreach (Requires r in proc.Requires) {
-              new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition);
+              new EnabledReplacementVisitor(fpIdentifierExpr).VisitExpr(r.Condition);
+              if (!QKeyValue.FindBoolAttribute(r.Attributes, "do_not_predicate")) {
+                r.Condition = Expr.Imp(fpIdentifierExpr, r.Condition);
+              }
             }
             foreach (Ensures e in proc.Ensures) {
               new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition);
+              if (!QKeyValue.FindBoolAttribute(e.Attributes, "do_not_predicate")) {
+                e.Condition = Expr.Imp(fpIdentifierExpr, e.Condition);
+              }
             }
           }
         }