Added /trustPhasesDownto option

2 files changed, 9 insertions, 1 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 00f830f9..911258ff 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -1258,7 +1258,7 @@ namespace Microsoft.Boogie
             Program program = linearTypeChecker.program;

             foreach (int phaseNum in moverTypeChecker.allPhaseNums)

             {

-                if (phaseNum <= CommandLineOptions.Clo.TrustPhasesUpto) continue;

+                if (CommandLineOptions.Clo.TrustPhasesDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustPhasesUpto) continue;

 

                 MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum);

                 List<Implementation> impls = new List<Implementation>();

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 0d254ab7..5de10eb2 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -490,6 +490,7 @@ namespace Microsoft.Boogie {
     public string OwickiGriesDesugaredOutputFile = null;

     public bool TrustAtomicityTypes = false;

     public int TrustPhasesUpto = -1;

+    public int TrustPhasesDownto = int.MaxValue;

 

     public enum VCVariety {

       Structured,

@@ -742,6 +743,13 @@ namespace Microsoft.Boogie {
           }

           return true;

 

+        case "trustPhasesDownto":

+          if (ps.ConfirmArgumentCount(1))

+          {

+              ps.GetNumericArgument(ref TrustPhasesDownto);

+          }

+          return true;

+

         case "proverLog":

           if (ps.ConfirmArgumentCount(1)) {

             SimplifyLogFilePath = args[ps.i];