diff options
| author |  Unknown <akashl@akash-desk.fareast.corp.microsoft.com> | 2013-01-03 16:53:59 +0530 |
|---|---|---|
| committer | Unknown <akashl@akash-desk.fareast.corp.microsoft.com> | 2013-01-03 16:53:59 +0530 |
| commit | 562c3d3af84d7c364fb6aa81cca83ff17bad64d2 (patch) | |
| tree | 4f81ee47d50bbc175262c428985fc85d1cbf73c6 /Source/Provers/SMTLib/SMTLibProverOptions.cs | |
| parent | bb3fd5a585f9f1be3100752f298ad633ff2624c4 (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.cs | 2 |
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();
}
|