diff options
| author |  qadeer <unknown> | 2010-04-30 21:52:45 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-04-30 21:52:45 +0000 |
| commit | 073a72e337da812d3e905aec31bcb17399ae34fc (patch) | |
| tree | fd85cf9bb548ab3750a37eabfa3343a2d79474f6 /Source/Provers/Z3/Prover.ssc | |
| parent | 185e797c7c662537fb40a51cc99d2266b0324c70 (diff) | |
1. Fixed lazy inlining implementation so that inlined procedures use live variable analysis as well
2. Separeted model printing from the lazy inlining option
Diffstat (limited to 'Source/Provers/Z3/Prover.ssc')
| -rw-r--r-- | Source/Provers/Z3/Prover.ssc | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc index 1da24532..f453d71d 100644 --- a/Source/Provers/Z3/Prover.ssc +++ b/Source/Provers/Z3/Prover.ssc @@ -110,7 +110,10 @@ namespace Microsoft.Boogie.Z3 }
}
}
- if (CommandLineOptions.Clo.PrintErrorModel >= 1 || CommandLineOptions.Clo.EnhancedErrorMessages == 1 || CommandLineOptions.Clo.ContractInfer) {
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 ||
+ CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
+ CommandLineOptions.Clo.ContractInfer ||
+ CommandLineOptions.Clo.LazyInlining) {
z3args += " " + OptionChar() + "m";
expectingModel = true;
}
|