diff options
author | 2013-07-16 09:39:07 +0100 | |
---|---|---|
committer | 2013-07-16 09:39:07 +0100 | |
commit | 581cade819b4b82ef344b32ba638fa6eb650a26b (patch) | |
tree | eb3f23ab1c90ba39882d6ec84a955c2fed4982a6 /Source/Core | |
parent | 035abd7ec2a774c8a721f7c39d58224fdcd123e2 (diff) |
Reworking of Staged Houdini in preparation for parallelising it.
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/CommandLineOptions.cs | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 37d5b51b..fcb3157b 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -397,7 +397,7 @@ namespace Microsoft.Boogie { public bool ContractInfer = false;
public bool ExplainHoudini = false;
public bool HoudiniUseCrossDependencies = false;
- public int StagedHoudini = 0;
+ public string StagedHoudini = null;
public bool DebugStagedHoudini = false;
public bool StagedHoudiniReachabilityAnalysis = false;
public bool StagedHoudiniMergeIgnoredCandidates = false;
@@ -889,12 +889,17 @@ namespace Microsoft.Boogie { }
case "stagedHoudini": {
- int sh = 0;
- if (ps.GetNumericArgument(ref sh, 4)) {
- StagedHoudini = sh;
+ if (ps.ConfirmArgumentCount(1)) {
+ if(args[ps.i] == "COARSE" ||
+ args[ps.i] == "FINE" ||
+ args[ps.i] == "BALANCED") {
+ StagedHoudini = args[ps.i];
+ } else {
+ ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
+ }
}
return true;
- }
+ }
case "stagedHoudiniReachabilityAnalysis": {
if (ps.ConfirmArgumentCount(0)) {
|