diff options
| author |  rustanleino <unknown> | 2010-09-23 02:03:11 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-09-23 02:03:11 +0000 |
| commit | a3d28fd0c7d454667b6bea71a34b89e47b66d611 (patch) | |
| tree | c8ab912181bd5b57ae8675744687a1feb1020273 /Source/Provers/Z3/Prover.cs | |
| parent | 40021fe7042eb08ed5b4d16034e23c9ed022c4aa (diff) | |
Boogie:
* Added /mv flag as the start of a Boogie replacement for /cev
* Allow attributes on assume statements
* /mv looks for the assume-statement attribute :captureState with a string-literal argument
Diffstat (limited to 'Source/Provers/Z3/Prover.cs')
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index a36ca87a..33e622ba 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -70,6 +70,7 @@ namespace Microsoft.Boogie.Z3 {
return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
+ CommandLineOptions.Clo.ModelView > 0 ||
CommandLineOptions.Clo.ContractInfer ||
CommandLineOptions.Clo.LazyInlining > 0 ||
CommandLineOptions.Clo.StratifiedInlining > 0;
|