From bf2a30fd04828fcf3480707ba2916a4d037a4cf3 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Mon, 24 Feb 2014 12:58:19 -0800
Subject: Added /trustPhasesDownto option

---
 Source/Concurrency/OwickiGries.cs | 2 +-
 Source/Core/CommandLineOptions.cs | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

(limited to 'Source')

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];
-- 
cgit v1.2.3