summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar allydonaldson <unknown>2013-07-16 09:39:07 +0100
committerGravatar allydonaldson <unknown>2013-07-16 09:39:07 +0100
commit581cade819b4b82ef344b32ba638fa6eb650a26b (patch)
treeeb3f23ab1c90ba39882d6ec84a955c2fed4982a6 /Source/Core
parent035abd7ec2a774c8a721f7c39d58224fdcd123e2 (diff)
Reworking of Staged Houdini in preparation for parallelising it.
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/CommandLineOptions.cs15
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)) {