diff options
| author |  MichalMoskal <unknown> | 2011-02-18 22:05:26 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-18 22:05:26 +0000 |
| commit | 2c6cf724d62c22362bfba6aeef73cd7d105e0c24 (patch) | |
| tree | 842e2d23f56a210335a4c51f94ebbb4dda7ef09d /Source/Provers/SMTLib/SMTLibProverOptions.cs | |
| parent | cdc6249dde1ee1153e1831380c3003af0b1cb9bc (diff) | |
Ask Z3 to generate models, in V2 format, when needed
Add supported :prover commands
Minor fixes
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibProverOptions.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 0565e677..76bce71c 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -39,6 +39,16 @@ namespace Microsoft.Boogie.SMTLib public string Inspector = null;
public bool OptimizeForBv = false;
+ 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;
+ }
+
public void AddSolverArgument(string s)
{
SolverArguments.Add(s);
|