inlining is now done in rhs of assignments for codeexprs

added more regressions

1 files changed, 21 insertions, 0 deletions

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index f3ac98a6..61b3a322 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -353,6 +353,27 @@ namespace Microsoft.Boogie {
                     newCmds.Add(codeCopier.CopyCmd(predCmd));

                 }

             }

+            else if (cmd is AssignCmd)

+            {

+                AssignCmd assignCmd = (AssignCmd)cmd;

+                this.inlinedSomething = false;

+                List<Expr> newRhss = new List<Expr>();

+                foreach (Expr rhsExpr in assignCmd.Rhss)

+                {

+                    newRhss.Add(this.VisitExpr(rhsExpr));

+                }

+                if (this.inlinedSomething)

+                {

+                    inlinedSomething = true;

+                    AssignCmd newAssignCmd = (AssignCmd)codeCopier.CopyCmd(assignCmd);

+                    newAssignCmd.Rhss = newRhss;

+                    newCmds.Add(newAssignCmd);

+                }

+                else

+                {

+                    newCmds.Add(codeCopier.CopyCmd(assignCmd));

+                }

+            }

             else

             {

                 newCmds.Add(codeCopier.CopyCmd(cmd));