fixed crash reported by Dan.

DoModSetAnalysis needs to run before the linear and mover type checking.

1 files changed, 6 insertions, 6 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ab1e185c..7756973d 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -505,12 +505,6 @@ namespace Microsoft.Boogie
           }

         }

 

-        EliminateDeadVariables(program);

-

-        CollectModSets(program);

-

-        CoalesceBlocks(program);

-

         if (CommandLineOptions.Clo.StratifiedInlining == 0)

         {

           Concurrency.Transform(linearTypeChecker, moverTypeChecker);

@@ -524,6 +518,10 @@ namespace Microsoft.Boogie
           }

         }

 

+        EliminateDeadVariables(program);

+

+        CoalesceBlocks(program);

+

         Inline(program);

 

         var stats = new PipelineStatistics();

@@ -742,6 +740,8 @@ namespace Microsoft.Boogie
           CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;

       }

 

+      CollectModSets(program);

+

       moverTypeChecker = new MoverTypeChecker(program);

       moverTypeChecker.TypeCheck();

       if (moverTypeChecker.errorCount != 0)