summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SMTLibProverOptions.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibProverOptions.cs')
-rw-r--r--Source/Provers/SMTLib/SMTLibProverOptions.cs10
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);