Fix mod-set traversal to do visit code inside code expressions.

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index d51fcdb3..31121093 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -200,6 +200,11 @@ namespace Microsoft.Boogie {
       moreProcessingRequired = true;

       modSets[localProc].Add(var);

     }

+    public override Expr VisitCodeExpr(CodeExpr node) {

+      // don't go into the code expression, since it can only modify variables local to the code expression,

+      // and the mod-set analysis is interested in global variables

+      return node;

+    }

   }

 

   public class VariableCollector : StandardVisitor {