diff options
| author |  akashlal <unknown> | 2011-11-26 10:15:25 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2011-11-26 10:15:25 +0530 |
| commit | dac5dec6e7283daaf4b357fb9c2edb1517a12f94 (patch) | |
| tree | b434620d911842eeecef2bc6b0f47c8cdb15e957 /Source/Provers/SMTLib/SMTLibProverOptions.cs | |
| parent | 19ce26677bba57940e3b41eba7d6dc4f0627e84c (diff) | |
Added option of turning off model generation in SI. Can be very expensive sometimes.
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibProverOptions.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 653b2c15..036b1f4a 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -43,12 +43,12 @@ namespace Microsoft.Boogie.SMTLib public bool ExpectingModel()
{
- return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
- CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
- CommandLineOptions.Clo.ModelViewFile != null ||
- CommandLineOptions.Clo.ContractInfer ||
- CommandLineOptions.Clo.LazyInlining > 0 ||
- CommandLineOptions.Clo.StratifiedInlining > 0;
+ return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
+ CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
+ CommandLineOptions.Clo.ModelViewFile != null ||
+ CommandLineOptions.Clo.ContractInfer ||
+ CommandLineOptions.Clo.LazyInlining > 0 ||
+ (CommandLineOptions.Clo.StratifiedInlining > 0 && !CommandLineOptions.Clo.StratifiedInliningWithoutModels);
}
public void AddSolverArgument(string s)
|