a fix regarding the checking of assertions in atomic specs at call sites

1 files changed, 1 insertions, 20 deletions

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 24e5f437..713d7068 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -94,24 +94,6 @@ namespace Microsoft.Boogie
 #endif

         }

 

-        private static HashSet<int> ComputePhaseIntervals(MoverTypeChecker moverTypeChecker)

-        {

-            HashSet<int> phases = new HashSet<int>();

-            foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)

-            {

-                Procedure proc = decl as Procedure;

-                if (proc == null) continue;

-                int phaseNum = moverTypeChecker.FindPhaseNumber(proc);

-                if (phaseNum != int.MaxValue) phases.Add(moverTypeChecker.FindPhaseNumber(proc));

-

-            }

-            foreach (int phs in moverTypeChecker.assertionPhaseNums)

-            {

-                phases.Add(phs);

-            }

-            return phases;

-        }

-

         private static Tuple<Automaton<BvSet>, bool> IsYieldReachabilitySafe(Automaton<BvSet> implReachabilityCheckAutomaton, Implementation impl, MoverTypeChecker moverTypeChecker, int phaseNum)

         {

             List<BvSet> witnessSet;

@@ -187,10 +169,9 @@ namespace Microsoft.Boogie
             Program yieldTypeCheckedProgram = moverTypeChecker.program;

             YieldTypeChecker regExprToAuto = new YieldTypeChecker();

 

-            HashSet<int> phases = ComputePhaseIntervals(moverTypeChecker);

             YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(moverTypeChecker);

 

-            foreach (int yTypeCheckCurrentPhaseNum in phases) // take current phase check num from each interval

+            foreach (int yTypeCheckCurrentPhaseNum in moverTypeChecker.allPhaseNums) // take current phase check num from each interval

             {

                 foreach (var decl in yieldTypeCheckedProgram.TopLevelDeclarations)

                 {