A simplification to predication of requires and ensures.

1 files changed, 2 insertions, 6 deletions

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 9478595b..2150f72d 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -494,15 +494,11 @@ public class SmartBlockPredicator {
               .ToArray());

 

           if (impl == null) {

-            var newRequires = new RequiresSeq();

             foreach (Requires r in proc.Requires) {

-              newRequires.Add(new Requires(r.Free,

-                new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));

+              new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition);

             }

-            var newEnsures = new EnsuresSeq();

             foreach (Ensures e in proc.Ensures) {

-              newEnsures.Add(new Ensures(e.Free,

-                new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));

+              new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition);

             }

           }

         }