another edit for predication

2 files changed, 20 insertions, 13 deletions

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index 345c0365..7ce38fd3 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -70,17 +70,21 @@ public class BlockPredicator {
                        new IfThenElse(Token.NoToken),
                        new ExprSeq(p, rhs, lhs.AsExpr))))));
     } else if (cmd is AssertCmd) {
-      var aCmd = (AssertCmd)cmd;
+      var aCmd = (AssertCmd)cmd;

       if (cmdSeq.Last() is AssignCmd &&
           cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) {
         // This may be a loop invariant.  Make sure it continues to appear as
         // the first statement in the block.
         var assign = cmdSeq.Last();
-        cmdSeq.Truncate(cmdSeq.Length-1);
-        cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
+        cmdSeq.Truncate(cmdSeq.Length-1);

+        aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);

+        cmdSeq.Add(aCmd);

+        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
         cmdSeq.Add(assign);
-      } else {
-        cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));
+      } else {

+        aCmd.Expr = Expr.Imp(p, aCmd.Expr);

+        cmdSeq.Add(aCmd);

+        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));
       }
     } else if (cmd is AssumeCmd) {
       var aCmd = (AssumeCmd)cmd;
@@ -113,7 +117,10 @@ public class BlockPredicator {
       Debug.Assert(useProcedurePredicates);
       var cCmd = (CallCmd)cmd;
       cCmd.Ins.Insert(0, p);
-      cmdSeq.Add(cCmd);
+      cmdSeq.Add(cCmd);

+    }

+    else if (cmd is CommentCmd) {

+      // skip

     } else {
       Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
     }
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 18417830..69337931 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1403,12 +1403,6 @@ namespace VC {
 

       ConvertCFG2DAG(impl);

 

-      if (CommandLineOptions.Clo.DoPredication) {

-        DesugarCalls(impl);

-        BlockPredicator.Predicate(program, impl);

-        impl.ComputePredecessorsForBlocks();

-      }

-

       SmokeTester smoke_tester = null;

       if (CommandLineOptions.Clo.SoundnessSmokeTest) {

         smoke_tester = new SmokeTester(this, impl, program, callback);

@@ -2061,7 +2055,13 @@ namespace VC {
         EmitImpl(impl, true);

       }

       #endregion

-    

+

+      if (CommandLineOptions.Clo.DoPredication) {

+        DesugarCalls(impl);

+        BlockPredicator.Predicate(program, impl);

+        impl.ComputePredecessorsForBlocks();

+      }

+

       if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {

         Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

       }