1 files changed, 34 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index a4374623..98086cf0 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -488,6 +488,12 @@ namespace Microsoft.Boogie {
     public int  /*0..9*/StepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator
 
     public string OwickiGriesDesugaredOutputFile = null;
+    public bool TrustAtomicityTypes = false;
+    public bool TrustNonInterference = false;
+    public int TrustPhasesUpto = -1;
+    public int TrustPhasesDownto = int.MaxValue;
+
+    public bool UseParallelism = true;
 
     public enum VCVariety {
       Structured,
@@ -605,6 +611,10 @@ namespace Microsoft.Boogie {
        Call
     };
     public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure;
+		
+    public string PrintFixedPoint = null;
+		
+    public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)
 
     public enum TypeEncoding {
       None,
@@ -733,6 +743,20 @@ namespace Microsoft.Boogie {
           }
           return true;
 
+        case "trustPhasesUpto":
+          if (ps.ConfirmArgumentCount(1))
+          {
+              ps.GetNumericArgument(ref TrustPhasesUpto);
+          }
+          return true;
+
+        case "trustPhasesDownto":
+          if (ps.ConfirmArgumentCount(1))
+          {
+              ps.GetNumericArgument(ref TrustPhasesDownto);
+          }
+          return true;
+
         case "proverLog":
           if (ps.ConfirmArgumentCount(1)) {
             SimplifyLogFilePath = args[ps.i];
@@ -1105,6 +1129,12 @@ namespace Microsoft.Boogie {
               }
           }
           return true;
+        case "printFixedPoint":
+          if (ps.ConfirmArgumentCount(1))
+          {
+              PrintFixedPoint = args[ps.i];
+          }
+          return true;
         case "siVerbose":
           if (ps.ConfirmArgumentCount(1)) {
             StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));
@@ -1371,7 +1401,10 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
               ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
               ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots) ||
-              ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately)
+              ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) ||
+              ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) ||
+              ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) ||
+              ps.CheckBooleanFlag("doNotUseParallelism", ref UseParallelism, false)
               ) {
             // one of the boolean flags matched
             return true;