More exhaustive generation of assertions during predication. Patch by Jeroen Ketema

1 files changed, 10 insertions, 4 deletions

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 37161f05..e31a1eb0 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -434,16 +434,22 @@ public class SmartBlockPredicator {
       prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { block });

     }

 

-    if (parentMap.ContainsKey(block)) {

-      var parent = parentMap[block];

+    Block currentBlock = block;

+    Expr pCurrentExpr = pExpr;

+    while (parentMap.ContainsKey(currentBlock)) {

+      Block parent = parentMap[currentBlock];

+      Expr pParentExpr = null;

       if (predMap.ContainsKey(parent)) {

         var parentPred = predMap[parent];

         if (parentPred != null) {

+          pParentExpr = Expr.Ident(parentPred);

           block.Cmds.Add(new AssertCmd(Token.NoToken,

-                                          pExpr != null ? (Expr)Expr.Imp(pExpr, Expr.Ident(parentPred))

-                                                        : Expr.Ident(parentPred)));

+                                          pCurrentExpr != null ? (Expr)Expr.Imp(pCurrentExpr, pParentExpr)

+                                                               : pParentExpr));

         }

       }

+      currentBlock = parent;

+      pCurrentExpr = pParentExpr;

     }

 

     var transferCmd = block.TransferCmd;