Block predicator: handle StateCmd

1 files changed, 7 insertions, 0 deletions

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index f4e82182..987574be 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -114,6 +114,13 @@ public class BlockPredicator {
       var cCmd = (CallCmd)cmd;
       cCmd.Ins.Insert(0, p);
       cmdSeq.Add(cCmd);
+    } else if (cmd is StateCmd) {
+      var sCmd = (StateCmd)cmd;
+      var newCmdSeq = new CmdSeq();
+      foreach (Cmd c in sCmd.Cmds)
+        PredicateCmd(newCmdSeq, c);
+      sCmd.Cmds = newCmdSeq;
+      cmdSeq.Add(sCmd);
     } else {
       Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
     }