summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SMTLibProverOptions.cs
diff options
context:
space:
mode:
authorGravatar Unknown <akashl@akash-desk.fareast.corp.microsoft.com>2013-01-03 16:53:59 +0530
committerGravatar Unknown <akashl@akash-desk.fareast.corp.microsoft.com>2013-01-03 16:53:59 +0530
commit562c3d3af84d7c364fb6aa81cca83ff17bad64d2 (patch)
tree4f81ee47d50bbc175262c428985fc85d1cbf73c6 /Source/Provers/SMTLib/SMTLibProverOptions.cs
parentbb3fd5a585f9f1be3100752f298ad633ff2624c4 (diff)
Use the new ProverInterface's Evaluate method in stratified inlinig
(guarded by the flag /useProverEvaluate)
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibProverOptions.cs')
-rw-r--r--Source/Provers/SMTLib/SMTLibProverOptions.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index b1cef239..d336252e 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -45,7 +45,7 @@ namespace Microsoft.Boogie.SMTLib
public bool OptimizeForBv = false;
public bool ProduceModel() {
- return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini ||
+ return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate ||
ExpectingModel();
}