Did some refactoring.

2 files changed, 9 insertions, 10 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index a9220a4c..093f1d90 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -467,7 +467,7 @@ namespace Microsoft.Boogie
 

         if (CommandLineOptions.Clo.PrintCFGPrefix != null)

         {

-          foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())

+          foreach (var impl in program.Implementations)

           {

             using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot"))

             {

@@ -868,7 +868,7 @@ namespace Microsoft.Boogie
 

       #region Select and prioritize implementations that should be verified

 

-      var impls = program.TopLevelDeclarations.OfType<Implementation>().Where(

+      var impls = program.Implementations.Where(

         impl => impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification);

 

       // operate on a stable copy, in case it gets updated while we're running

@@ -876,7 +876,7 @@ namespace Microsoft.Boogie
       if (0 < CommandLineOptions.Clo.VerifySnapshots)

       {

         // TODO(wuestholz): Maybe we should speed up this lookup.

-        OtherDefinitionAxiomsCollector.Collect(program.TopLevelDeclarations.OfType<Axiom>());

+        OtherDefinitionAxiomsCollector.Collect(program.Axioms);

         DependencyCollector.Collect(program);

         stablePrioritizedImpls = impls.OrderByDescending(

           impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();

@@ -1084,10 +1084,9 @@ namespace Microsoft.Boogie
               var svcgen = vcgen as VC.StratifiedVCGen;

               Contract.Assert(svcgen != null);

               var ss = new HashSet<string>();

-              foreach (var tdecl in program.TopLevelDeclarations)

+              foreach (var c in program.Constants)

               {

-                var c = tdecl as Constant;

-                if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

+                if (!c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

                 ss.Add(c.Name);

               }

               verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 55c6ba85..93ca9cb7 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -194,7 +194,7 @@ namespace Microsoft.Boogie
     private static void SetAssertionChecksums(Implementation implementation, Program program)

     {

       // TODO(wuestholz): Maybe we should speed up this lookup.

-      var implPrevSnap = program.Implementations().FirstOrDefault(i => i.Id == implementation.Id);

+      var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id);

       if (implPrevSnap != null)

       {

         implementation.AssertionChecksums = implPrevSnap.AssertionChecksums;

@@ -204,7 +204,7 @@ namespace Microsoft.Boogie
     private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program)

     {

       // TODO(wuestholz): Maybe we should speed up this lookup.

-      var implPrevSnap = program.Implementations().FirstOrDefault(i => i.Id == implementation.Id);

+      var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id);

       if (implPrevSnap != null)

       {

         implementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums;

@@ -216,7 +216,7 @@ namespace Microsoft.Boogie
       var result = base.VisitCallCmd(node);

 

       // TODO(wuestholz): Maybe we should speed up this lookup.

-      var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);

+      var oldProc = programInCachedSnapshot.Procedures.FirstOrDefault(p => p.Name == node.Proc.Name);

       if (oldProc != null

           && oldProc.DependencyChecksum != node.Proc.DependencyChecksum

           && node.AssignedAssumptionVariable == null)

@@ -327,7 +327,7 @@ namespace Microsoft.Boogie
       Contract.Requires(oldProc != null && newProg != null);

 

       // TODO(wuestholz): Maybe we should speed up this lookup.

-      var funcs = newProg.TopLevelDeclarations.OfType<Function>();

+      var funcs = newProg.Functions;

       return oldProc.DependenciesCollected

              && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)));

     }