summaryrefslogtreecommitdiff
path: root/Source/Core/CommandLineOptions.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
-rw-r--r--Source/Core/CommandLineOptions.cs3
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) ||