diff options
author | Valentin Wüstholz <wuestholz@gmail.com> | 2015-11-16 12:04:37 -0600 |
---|---|---|
committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-11-16 12:04:37 -0600 |
commit | f049d2ec646244bc40964b36d961966fe2a3e4dc (patch) | |
tree | 31dd22334b5cb314eb018fd1deee810836ffa486 /Source/Core/CommandLineOptions.cs | |
parent | 74765d1b66730a612ce3eaf404883c09ab8f0153 (diff) |
Add support for identifying unnecessary assumes.
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
-rw-r--r-- | Source/Core/CommandLineOptions.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 3892bbc0..e9aa3ceb 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -479,6 +479,8 @@ namespace Microsoft.Boogie { public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; public bool PrintAssignment = false; + // TODO(wuestholz): Add documentation for this flag. + public bool PrintNecessaryAssumes = false; public int InlineDepth = -1; public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values public bool UseUncheckedContracts = false; @@ -1619,6 +1621,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) || ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) || ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || + ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) || ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) || ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) || ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) || |