diff options
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 2 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 8 |
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];
|